Solving ../../benchmarks/false/sort_bug_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, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja])
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))])}
(insert([_ija, _jja, _kja]) /\ insert([_ija, _jja, _lja])) -> eq_eltlist([_kja, _lja])
)
(sort, F:
{() -> sort([nil, nil])
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja])}
(sort([_oja, _pja]) /\ sort([_oja, _qja])) -> eq_eltlist([_pja, _qja])
)
(length, F:
{() -> length([nil, z])
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)])}
(length([_sja, _tja]) /\ length([_sja, _uja])) -> eq_nat([_tja, _uja])
)
}

properties:
{(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja])}


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

Clause system for inference is:

{
() -> insert([x, nil, cons(x, nil)]) -> 0
() -> length([nil, z]) -> 0
() -> leq([a, y]) -> 0
() -> leq([b, b]) -> 0
() -> sort([nil, nil]) -> 0
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 0
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 0
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 0
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 0
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 0
(leq([b, a])) -> BOT -> 0
}


Solving took 2.462103 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004981 s (model generation: 0.003851,  model checking: 0.001130):

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
}}}
  ;  sort -> 
{{{
Q={},
Q_f={},
Delta=
{

}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> sort([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.004016 s (model generation: 0.003980,  model checking: 0.000036):

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
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([b, b]), {

})

-------------------------------------------
Step 2, which took 0.004784 s (model generation: 0.004682,  model checking: 0.000102):

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_6618},
Q_f={q_gen_6618},
Delta=
{
<b, b>() -> q_gen_6618
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([a, y]), {
y -> b
})

-------------------------------------------
Step 3, which took 0.006535 s (model generation: 0.006398,  model checking: 0.000137):

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_6618},
Q_f={q_gen_6618},
Delta=
{
<a, b>() -> q_gen_6618
<b, b>() -> q_gen_6618
}

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 4, which took 0.011438 s (model generation: 0.011166,  model checking: 0.000272):

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

}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 1
(leq([b, a])) -> BOT -> 1
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> b
})

-------------------------------------------
Step 5, which took 0.015136 s (model generation: 0.011103,  model checking: 0.004033):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 1
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> 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 6, which took 0.011643 s (model generation: 0.011438,  model checking: 0.000205):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<b, b>() -> q_gen_6626
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 1
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 1
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _rja])) -> length([cons(x, ll), s(_rja)]), {
_rja -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 7, which took 0.012098 s (model generation: 0.011655,  model checking: 0.000443):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<b, b>() -> q_gen_6626
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617},
Q_f={q_gen_6617},
Delta=
{
<nil, nil>() -> q_gen_6617
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 1
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 2
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(b, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 8, which took 0.013810 s (model generation: 0.011691,  model checking: 0.002119):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<b, b>() -> q_gen_6626
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 2
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 2
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 9, which took 0.012488 s (model generation: 0.012458,  model checking: 0.000030):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, b>() -> q_gen_6626
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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
() -> sort([nil, nil]) -> 3
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 2
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((leq([b, a])) -> BOT, {

})

-------------------------------------------
Step 10, which took 0.012815 s (model generation: 0.012435,  model checking: 0.000380):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, b>() -> q_gen_6626
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 3
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: (() -> leq([a, y]), {
y -> a
})

-------------------------------------------
Step 11, which took 0.015108 s (model generation: 0.012725,  model checking: 0.002383):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, b>() -> q_gen_6626
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 4
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 4
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: (() -> insert([x, nil, cons(x, nil)]), {
x -> a
})

-------------------------------------------
Step 12, which took 0.014303 s (model generation: 0.012983,  model checking: 0.001320):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 4
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 4
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 13, which took 0.013750 s (model generation: 0.013373,  model checking: 0.000377):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 4
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 4
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _rja])) -> length([cons(x, ll), s(_rja)]), {
_rja -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 14, which took 0.015534 s (model generation: 0.013732,  model checking: 0.001802):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 4
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 7
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 5
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(b, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 15, which took 0.015285 s (model generation: 0.014675,  model checking: 0.000610):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 6
() -> length([nil, z]) -> 4
() -> leq([a, y]) -> 6
() -> leq([b, b]) -> 4
() -> sort([nil, nil]) -> 4
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 7
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 7
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 5
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 7
(leq([b, a])) -> BOT -> 5
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(a, nil)  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 16, which took 0.018403 s (model generation: 0.016534,  model checking: 0.001869):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 7
() -> length([nil, z]) -> 5
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 5
() -> sort([nil, nil]) -> 5
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 7
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 7
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 6
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 7
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 6
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 17, which took 0.018516 s (model generation: 0.016892,  model checking: 0.001624):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 7
() -> length([nil, z]) -> 6
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 6
() -> sort([nil, nil]) -> 6
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 7
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 10
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 7
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 8
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 7
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(a, nil)  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 18, which took 0.018971 s (model generation: 0.017201,  model checking: 0.001770):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 7
() -> length([nil, z]) -> 7
() -> leq([a, y]) -> 7
() -> leq([b, b]) -> 7
() -> sort([nil, nil]) -> 7
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 10
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 10
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 8
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 8
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 10
(leq([b, a])) -> BOT -> 8
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 19, which took 0.021154 s (model generation: 0.018381,  model checking: 0.002773):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 8
() -> length([nil, z]) -> 8
() -> leq([a, y]) -> 8
() -> leq([b, b]) -> 8
() -> sort([nil, nil]) -> 8
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 10
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 13
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 9
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 9
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 9
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(a, nil)  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 20, which took 0.024524 s (model generation: 0.021617,  model checking: 0.002907):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 9
() -> length([nil, z]) -> 9
() -> leq([a, y]) -> 9
() -> leq([b, b]) -> 9
() -> sort([nil, nil]) -> 9
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 13
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 13
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 10
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 10
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 11
(leq([b, a])) -> BOT -> 10
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 21, which took 0.027457 s (model generation: 0.025049,  model checking: 0.002408):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630},
Q_f={q_gen_6617},
Delta=
{
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 10
() -> length([nil, z]) -> 10
() -> leq([a, y]) -> 10
() -> leq([b, b]) -> 10
() -> sort([nil, nil]) -> 10
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 13
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 16
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 11
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 11
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 12
(leq([b, a])) -> BOT -> 11
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(b, cons(b, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 22, which took 0.030095 s (model generation: 0.028374,  model checking: 0.001721):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
}

Datatype: <eltlist, eltlist>
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)]) -> 11
() -> length([nil, z]) -> 11
() -> leq([a, y]) -> 11
() -> leq([b, b]) -> 11
() -> sort([nil, nil]) -> 11
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 13
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 16
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 14
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 12
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 12
(leq([b, a])) -> BOT -> 12
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> z  ;  _wja -> cons(b, nil)  ;  _xja -> s(z)  ;  l -> nil
})

-------------------------------------------
Step 23, which took 0.031203 s (model generation: 0.028528,  model checking: 0.002675):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6663, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6663) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6663
}

Datatype: <eltlist, eltlist>
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)]) -> 12
() -> length([nil, z]) -> 12
() -> leq([a, y]) -> 12
() -> leq([b, b]) -> 12
() -> sort([nil, nil]) -> 12
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 14
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 16
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 17
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 13
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 13
(leq([b, a])) -> BOT -> 13
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> s(z)  ;  _wja -> cons(b, cons(b, nil))  ;  _xja -> s(s(z))  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.032934 s (model generation: 0.030043,  model checking: 0.002891):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6644, q_gen_6663, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6644, q_gen_6663) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<b, b>() -> q_gen_6630
<a, a>() -> q_gen_6644
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
<cons, cons>(q_gen_6630, q_gen_6663) -> q_gen_6663
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6663
}

Datatype: <eltlist, eltlist>
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)]) -> 13
() -> length([nil, z]) -> 13
() -> leq([a, y]) -> 13
() -> leq([b, b]) -> 13
() -> sort([nil, nil]) -> 13
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 15
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 19
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 17
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 14
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 14
(leq([b, a])) -> BOT -> 14
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(b, cons(b, nil))  ;  y -> b  ;  z -> nil
})

-------------------------------------------
Step 25, which took 0.035615 s (model generation: 0.031439,  model checking: 0.004176):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 14
() -> length([nil, z]) -> 14
() -> leq([a, y]) -> 14
() -> leq([b, b]) -> 14
() -> sort([nil, nil]) -> 14
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 18
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 19
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 17
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 15
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 15
(leq([b, a])) -> BOT -> 15
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(a, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 26, which took 0.044555 s (model generation: 0.035222,  model checking: 0.009333):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 15
() -> length([nil, z]) -> 15
() -> leq([a, y]) -> 15
() -> leq([b, b]) -> 15
() -> sort([nil, nil]) -> 15
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 19
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 22
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 18
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 16
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 16
(leq([b, a])) -> BOT -> 16
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(b, nil)  ;  _nja -> cons(b, nil)  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 27, which took 0.042539 s (model generation: 0.040246,  model checking: 0.002293):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 16
() -> length([nil, z]) -> 16
() -> leq([a, y]) -> 16
() -> leq([b, b]) -> 16
() -> sort([nil, nil]) -> 16
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 19
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 22
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 21
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 17
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 17
(leq([b, a])) -> BOT -> 17
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> s(z)  ;  _wja -> nil  ;  _xja -> z  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 0.042135 s (model generation: 0.040717,  model checking: 0.001418):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6620, q_gen_6627, q_gen_6628, q_gen_6666},
Q_f={q_gen_6620, q_gen_6627},
Delta=
{
<a>() -> q_gen_6628
<b>() -> q_gen_6628
<nil, z>() -> q_gen_6620
<cons, s>(q_gen_6628, q_gen_6620) -> q_gen_6627
<cons, s>(q_gen_6628, q_gen_6627) -> q_gen_6666
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6663, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6663) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6663
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6663
}

Datatype: <eltlist, eltlist>
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)]) -> 17
() -> length([nil, z]) -> 17
() -> leq([a, y]) -> 17
() -> leq([b, b]) -> 17
() -> sort([nil, nil]) -> 17
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 19
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 22
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 21
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 20
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 18
(leq([b, a])) -> BOT -> 18
}
Sat witness: Found: ((length([ll, _rja])) -> length([cons(x, ll), s(_rja)]), {
_rja -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 29, which took 0.043209 s (model generation: 0.041568,  model checking: 0.001641):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
}

Datatype: <elt, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_6620, q_gen_6627, q_gen_6628, q_gen_6641, q_gen_6666},
Q_f={q_gen_6620, q_gen_6627},
Delta=
{
<b>() -> q_gen_6628
<a>() -> q_gen_6641
<cons, s>(q_gen_6641, q_gen_6620) -> q_gen_6620
<nil, z>() -> q_gen_6620
<cons, s>(q_gen_6628, q_gen_6620) -> q_gen_6627
<cons, s>(q_gen_6628, q_gen_6627) -> q_gen_6666
}

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6663, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6663) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6663
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6663
}

Datatype: <eltlist, eltlist>
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)]) -> 18
() -> length([nil, z]) -> 18
() -> leq([a, y]) -> 18
() -> leq([b, b]) -> 18
() -> sort([nil, nil]) -> 18
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 20
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 22
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 21
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 23
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 19
(leq([b, a])) -> BOT -> 19
}
Sat witness: Found: ((length([ll, _rja])) -> length([cons(x, ll), s(_rja)]), {
_rja -> s(z)  ;  ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 30, which took 0.043802 s (model generation: 0.041562,  model checking: 0.002240):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665, q_gen_6675},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6675) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6675
}

Datatype: <eltlist, eltlist>
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)]) -> 19
() -> length([nil, z]) -> 19
() -> leq([a, y]) -> 19
() -> leq([b, b]) -> 19
() -> sort([nil, nil]) -> 19
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 23
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 22
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 21
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 23
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 20
(leq([b, a])) -> BOT -> 20
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(b, cons(b, cons(b, nil)))  ;  x -> b  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 31, which took 0.046183 s (model generation: 0.044618,  model checking: 0.001565):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665, q_gen_6675},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6675) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6675
}

Datatype: <eltlist, eltlist>
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)]) -> 20
() -> length([nil, z]) -> 20
() -> leq([a, y]) -> 20
() -> leq([b, b]) -> 20
() -> sort([nil, nil]) -> 20
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 23
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 22
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 24
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 23
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 21
(leq([b, a])) -> BOT -> 21
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> s(s(z))  ;  _wja -> cons(b, nil)  ;  _xja -> s(z)  ;  l -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 32, which took 0.047929 s (model generation: 0.045952,  model checking: 0.001977):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665, q_gen_6676},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<a>() -> q_gen_6676
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, nil>(q_gen_6676, q_gen_6664) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 21
() -> length([nil, z]) -> 21
() -> leq([a, y]) -> 21
() -> leq([b, b]) -> 21
() -> sort([nil, nil]) -> 21
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 23
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 25
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 24
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 23
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 22
(leq([b, a])) -> BOT -> 22
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(b, cons(b, cons(b, nil)))  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 33, which took 0.050290 s (model generation: 0.048123,  model checking: 0.002167):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665, q_gen_6676},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<a>() -> q_gen_6676
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, nil>(q_gen_6676, q_gen_6664) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 22
() -> length([nil, z]) -> 22
() -> leq([a, y]) -> 22
() -> leq([b, b]) -> 22
() -> sort([nil, nil]) -> 22
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 24
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 25
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 27
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 24
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 23
(leq([b, a])) -> BOT -> 23
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> s(z)  ;  _wja -> nil  ;  _xja -> z  ;  l -> cons(a, nil)
})

-------------------------------------------
Step 34, which took 0.049726 s (model generation: 0.048258,  model checking: 0.001468):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6656, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6656
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6656
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6656
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6656
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 23
() -> length([nil, z]) -> 23
() -> leq([a, y]) -> 23
() -> leq([b, b]) -> 23
() -> sort([nil, nil]) -> 23
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 24
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 25
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 27
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 24
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 26
(leq([b, a])) -> BOT -> 24
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 35, which took 0.057851 s (model generation: 0.052924,  model checking: 0.004927):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, nil>() -> q_gen_6625
<a, a>() -> q_gen_6626
<a, b>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665, q_gen_6675, q_gen_6676},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<a>() -> q_gen_6676
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6675) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
<cons, nil>(q_gen_6676, q_gen_6664) -> q_gen_6675
}

Datatype: <eltlist, eltlist>
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)]) -> 24
() -> length([nil, z]) -> 24
() -> leq([a, y]) -> 24
() -> leq([b, b]) -> 24
() -> sort([nil, nil]) -> 24
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 25
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 28
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 27
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 25
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 26
(leq([b, a])) -> BOT -> 25
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(b, nil)  ;  _nja -> cons(b, nil)  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 36, which took 0.052000 s (model generation: 0.049309,  model checking: 0.002691):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 25
() -> length([nil, z]) -> 25
() -> leq([a, y]) -> 25
() -> leq([b, b]) -> 25
() -> sort([nil, nil]) -> 25
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 28
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 28
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 27
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 26
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 26
(leq([b, a])) -> BOT -> 26
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(a, cons(b, cons(b, nil)))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 37, which took 0.036408 s (model generation: 0.034916,  model checking: 0.001492):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6660, q_gen_6661},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<a>() -> q_gen_6623
<b>() -> q_gen_6623
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6661
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6661
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6662, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6662) -> q_gen_6662
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6662
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6662
}

Datatype: <eltlist, eltlist>
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)]) -> 26
() -> length([nil, z]) -> 26
() -> leq([a, y]) -> 26
() -> leq([b, b]) -> 26
() -> sort([nil, nil]) -> 26
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 28
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 31
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 28
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 27
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 27
(leq([b, a])) -> BOT -> 27
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(a, nil)  ;  _nja -> cons(b, nil)  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 38, which took 0.048395 s (model generation: 0.046639,  model checking: 0.001756):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 27
() -> length([nil, z]) -> 27
() -> leq([a, y]) -> 27
() -> leq([b, b]) -> 27
() -> sort([nil, nil]) -> 27
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 28
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 31
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 28
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 27
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 30
(leq([b, a])) -> BOT -> 28
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 39, which took 0.059185 s (model generation: 0.057308,  model checking: 0.001877):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6642, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6642
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6642
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6642
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6643, q_gen_6644, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6644, q_gen_6643) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6643) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6643
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6643
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6643
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
}

Datatype: <eltlist, eltlist>
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)]) -> 28
() -> length([nil, z]) -> 28
() -> leq([a, y]) -> 28
() -> leq([b, b]) -> 28
() -> sort([nil, nil]) -> 28
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 28
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 31
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 31
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 28
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 30
(leq([b, a])) -> BOT -> 29
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> s(z)  ;  _wja -> cons(a, cons(b, nil))  ;  _xja -> s(s(z))  ;  l -> cons(b, nil)
})

-------------------------------------------
Step 40, which took 0.064339 s (model generation: 0.059404,  model checking: 0.004935):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6642, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6642
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6642
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6642
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6643, q_gen_6644, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6643) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6643) -> q_gen_6643
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6643
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6643
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
}

Datatype: <eltlist, eltlist>
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)]) -> 28
() -> length([nil, z]) -> 28
() -> leq([a, y]) -> 28
() -> leq([b, b]) -> 28
() -> sort([nil, nil]) -> 28
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 31
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 31
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 31
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 29
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 30
(leq([b, a])) -> BOT -> 29
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(a, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 41, which took 0.057026 s (model generation: 0.056318,  model checking: 0.000708):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6642, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6642
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6642
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6642
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6643, q_gen_6644, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6643) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6643) -> q_gen_6643
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6643
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6643
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
}

Datatype: <eltlist, eltlist>
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)]) -> 29
() -> length([nil, z]) -> 29
() -> leq([a, y]) -> 29
() -> leq([b, b]) -> 29
() -> sort([nil, nil]) -> 29
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 31
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 31
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 31
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 30
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 33
(leq([b, a])) -> BOT -> 30
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 42, which took 0.062575 s (model generation: 0.060480,  model checking: 0.002095):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6642, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6625
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, a>() -> q_gen_6634
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6642
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6642
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6642
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6643, q_gen_6644, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6643) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6643) -> q_gen_6643
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6643
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6643
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
}

Datatype: <eltlist, eltlist>
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)]) -> 30
() -> length([nil, z]) -> 30
() -> leq([a, y]) -> 30
() -> leq([b, b]) -> 30
() -> sort([nil, nil]) -> 30
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 31
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 34
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 32
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 31
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 33
(leq([b, a])) -> BOT -> 31
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(a, nil)  ;  _nja -> cons(a, nil)  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 43, which took 0.076342 s (model generation: 0.073969,  model checking: 0.002373):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6642, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6642
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6642
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6642
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6643, q_gen_6644, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6643) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6643) -> q_gen_6643
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6643
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6643
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
}

Datatype: <eltlist, eltlist>
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)]) -> 31
() -> length([nil, z]) -> 31
() -> leq([a, y]) -> 31
() -> leq([b, b]) -> 31
() -> sort([nil, nil]) -> 31
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 34
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 34
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 32
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 32
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 33
(leq([b, a])) -> BOT -> 32
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(b, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 44, which took 0.077907 s (model generation: 0.075000,  model checking: 0.002907):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 32
() -> length([nil, z]) -> 32
() -> leq([a, y]) -> 32
() -> leq([b, b]) -> 32
() -> sort([nil, nil]) -> 32
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 34
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 37
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 33
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 33
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 34
(leq([b, a])) -> BOT -> 33
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> nil  ;  _nja -> cons(a, cons(a, nil))  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 45, which took 0.085248 s (model generation: 0.082575,  model checking: 0.002673):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6642, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6642
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6642
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6642
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6642
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6642
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6643, q_gen_6644, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6643) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6617) -> q_gen_6643
<cons, cons>(q_gen_6644, q_gen_6643) -> q_gen_6643
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6643
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6643
<a, b>() -> q_gen_6644
<b, a>() -> q_gen_6644
}

Datatype: <eltlist, eltlist>
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)]) -> 33
() -> length([nil, z]) -> 33
() -> leq([a, y]) -> 33
() -> leq([b, b]) -> 33
() -> sort([nil, nil]) -> 33
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 37
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 37
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 34
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 34
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 35
(leq([b, a])) -> BOT -> 34
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(a, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 46, which took 0.094812 s (model generation: 0.092489,  model checking: 0.002323):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 34
() -> length([nil, z]) -> 34
() -> leq([a, y]) -> 34
() -> leq([b, b]) -> 34
() -> sort([nil, nil]) -> 34
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 37
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 40
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 35
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 35
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 36
(leq([b, a])) -> BOT -> 35
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(b, nil)  ;  _nja -> cons(b, cons(a, nil))  ;  y -> b  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 47, which took 0.095552 s (model generation: 0.093019,  model checking: 0.002533):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6633
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 35
() -> length([nil, z]) -> 35
() -> leq([a, y]) -> 35
() -> leq([b, b]) -> 35
() -> sort([nil, nil]) -> 35
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 40
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 40
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 36
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 36
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 37
(leq([b, a])) -> BOT -> 36
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(a, nil)  ;  x -> b  ;  y -> a  ;  z -> cons(a, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 48, which took 0.107324 s (model generation: 0.104324,  model checking: 0.003000):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6633
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<b, a>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6621
<a, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 36
() -> length([nil, z]) -> 36
() -> leq([a, y]) -> 36
() -> leq([b, b]) -> 36
() -> sort([nil, nil]) -> 36
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 40
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 43
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 37
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 37
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 38
(leq([b, a])) -> BOT -> 37
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(b, nil)  ;  _nja -> cons(a, nil)  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 49, which took 0.112332 s (model generation: 0.111050,  model checking: 0.001282):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 37
() -> length([nil, z]) -> 37
() -> leq([a, y]) -> 37
() -> leq([b, b]) -> 37
() -> sort([nil, nil]) -> 37
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 40
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 43
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 38
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 38
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 41
(leq([b, a])) -> BOT -> 38
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> a  ;  y -> a  ;  z -> nil
})

-------------------------------------------
Step 50, which took 0.110806 s (model generation: 0.109736,  model checking: 0.001070):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 38
() -> length([nil, z]) -> 38
() -> leq([a, y]) -> 38
() -> leq([b, b]) -> 38
() -> sort([nil, nil]) -> 38
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 43
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 43
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 39
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 39
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 41
(leq([b, a])) -> BOT -> 39
}
Sat witness: Found: ((insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]), {
_hja -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a  ;  z -> cons(b, nil)
})

-------------------------------------------
Step 51, which took 0.106434 s (model generation: 0.105438,  model checking: 0.000996):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 39
() -> length([nil, z]) -> 39
() -> leq([a, y]) -> 39
() -> leq([b, b]) -> 39
() -> sort([nil, nil]) -> 39
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 43
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 43
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 40
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 40
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 44
(leq([b, a])) -> BOT -> 40
}
Sat witness: Found: ((leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]), {
x -> b  ;  y -> b  ;  z -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 52, which took 0.114757 s (model generation: 0.112239,  model checking: 0.002518):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6622
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6664, q_gen_6665},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<a>() -> q_gen_6665
<b>() -> q_gen_6665
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6654
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
}

Datatype: <eltlist, eltlist>
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)]) -> 40
() -> length([nil, z]) -> 40
() -> leq([a, y]) -> 40
() -> leq([b, b]) -> 40
() -> sort([nil, nil]) -> 40
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 43
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 46
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 41
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 41
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 44
(leq([b, a])) -> BOT -> 41
}
Sat witness: Found: ((insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]), {
_mja -> cons(a, nil)  ;  _nja -> cons(b, nil)  ;  y -> b  ;  z -> cons(a, nil)
})

-------------------------------------------
Step 53, which took 0.118471 s (model generation: 0.117741,  model checking: 0.000730):

Model:
|_
{
insert -> 
{{{
Q={q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6625, q_gen_6626, q_gen_6633, q_gen_6634, q_gen_6637, q_gen_6645, q_gen_6660},
Q_f={q_gen_6621},
Delta=
{
<nil>() -> q_gen_6622
<b>() -> q_gen_6623
<a>() -> q_gen_6637
<cons>(q_gen_6623, q_gen_6622) -> q_gen_6660
<cons>(q_gen_6623, q_gen_6660) -> q_gen_6660
<cons>(q_gen_6637, q_gen_6622) -> q_gen_6660
<cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6625
<cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6625
<cons, nil>(q_gen_6637, q_gen_6622) -> q_gen_6625
<nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6625
<a, a>() -> q_gen_6626
<b, a>() -> q_gen_6626
<b, b>() -> q_gen_6626
<cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6622) -> q_gen_6633
<cons, nil>(q_gen_6623, q_gen_6660) -> q_gen_6633
<cons, nil>(q_gen_6637, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6633
<nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6633
<nil, nil>() -> q_gen_6633
<a, b>() -> q_gen_6634
<a, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<a, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6621
<b, cons, cons>(q_gen_6626, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6625) -> q_gen_6621
<b, cons, cons>(q_gen_6634, q_gen_6633) -> q_gen_6621
<b, nil, cons>(q_gen_6623, q_gen_6622) -> q_gen_6621
<a, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<a, nil, cons>(q_gen_6637, q_gen_6660) -> q_gen_6645
<b, cons, cons>(q_gen_6626, q_gen_6633) -> q_gen_6645
<b, nil, cons>(q_gen_6623, q_gen_6660) -> q_gen_6645
<b, nil, cons>(q_gen_6637, q_gen_6622) -> q_gen_6645
}

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

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

Datatype: <elt, elt>
Convolution form: right
}}}
  ;  sort -> 
{{{
Q={q_gen_6617, q_gen_6630, q_gen_6654, q_gen_6655, q_gen_6663, q_gen_6664, q_gen_6665, q_gen_6676},
Q_f={q_gen_6617},
Delta=
{
<nil>() -> q_gen_6664
<b>() -> q_gen_6665
<a>() -> q_gen_6676
<cons, cons>(q_gen_6630, q_gen_6617) -> q_gen_6617
<cons, cons>(q_gen_6630, q_gen_6654) -> q_gen_6617
<nil, nil>() -> q_gen_6617
<a, a>() -> q_gen_6630
<a, b>() -> q_gen_6630
<b, b>() -> q_gen_6630
<cons, cons>(q_gen_6630, q_gen_6663) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6617) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6654) -> q_gen_6654
<cons, cons>(q_gen_6655, q_gen_6663) -> q_gen_6654
<cons, nil>(q_gen_6676, q_gen_6664) -> q_gen_6654
<b, a>() -> q_gen_6655
<cons, nil>(q_gen_6665, q_gen_6664) -> q_gen_6663
<nil, cons>(q_gen_6665, q_gen_6664) -> q_gen_6663
<nil, cons>(q_gen_6676, q_gen_6664) -> q_gen_6663
}

Datatype: <eltlist, eltlist>
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)]) -> 41
() -> length([nil, z]) -> 41
() -> leq([a, y]) -> 41
() -> leq([b, b]) -> 41
() -> sort([nil, nil]) -> 41
(insert([x, z, _hja]) /\ not leq([x, y])) -> insert([x, cons(y, z), _hja]) -> 43
(insert([y, _mja, _nja]) /\ sort([z, _mja])) -> sort([cons(y, z), _nja]) -> 46
(length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]) -> 44
(length([ll, _rja])) -> length([cons(x, ll), s(_rja)]) -> 42
(leq([x, y])) -> insert([x, cons(y, z), cons(x, cons(y, z))]) -> 44
(leq([b, a])) -> BOT -> 42
}
Sat witness: Found: ((length([_wja, _xja]) /\ length([l, _vja]) /\ sort([l, _wja])) -> eq_nat([_vja, _xja]), {
_vja -> s(s(z))  ;  _wja -> cons(b, nil)  ;  _xja -> s(z)  ;  l -> cons(b, cons(a, nil))
})

Total time: 2.462103
Reason for stopping: Disproved