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:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)])}
(append([_la, _ma, _na]) /\ append([_la, _ma, _oa])) -> eq_eltlist([_na, _oa])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)])}
(length([_qa, _ra]) /\ length([_qa, _sa])) -> eq_nat([_ra, _sa])
)
}

properties:
{(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]), (append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya])}


over-approximation: {append, length}
under-approximation: {leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 0
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 0
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 0
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
}


Solving took 0.385935 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<cons>(q_gen_292, q_gen_291) -> q_gen_291
<nil>() -> q_gen_291
<a>() -> q_gen_292
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<a, b>() -> q_gen_280
<b, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<a, a, a>() -> q_gen_293
<a, b, a>() -> q_gen_293
<b, a, b>() -> q_gen_293
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010973 s (model generation: 0.010455,  model checking: 0.000518):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 1, which took 0.012487 s (model generation: 0.010688,  model checking: 0.001799):

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

}

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

}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.010514 s (model generation: 0.010394,  model checking: 0.000120):

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

}

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

}

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<z>() -> q_gen_272
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 3, which took 0.010643 s (model generation: 0.010357,  model checking: 0.000286):

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

}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<z>() -> q_gen_272
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 4, which took 0.010903 s (model generation: 0.010540,  model checking: 0.000363):

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

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<z>() -> q_gen_272
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 5, which took 0.010869 s (model generation: 0.010677,  model checking: 0.000192):

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

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 1
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 6, which took 0.021317 s (model generation: 0.011096,  model checking: 0.010221):

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

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 1
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 1
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.012023 s (model generation: 0.011321,  model checking: 0.000702):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280},
Q_f={q_gen_274},
Delta=
{
<nil, nil>() -> q_gen_279
<b, b>() -> q_gen_280
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 2
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 2
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 8, which took 0.014629 s (model generation: 0.011771,  model checking: 0.002858):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280},
Q_f={q_gen_274},
Delta=
{
<nil, nil>() -> q_gen_279
<b, b>() -> q_gen_280
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 3
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 3
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 9, which took 0.014338 s (model generation: 0.012300,  model checking: 0.002038):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280},
Q_f={q_gen_274},
Delta=
{
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 4
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 4
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 4
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _pa])) -> length([cons(x, ll), s(_pa)]), {
_pa -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 10, which took 0.015253 s (model generation: 0.012473,  model checking: 0.002780):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280},
Q_f={q_gen_274},
Delta=
{
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 4
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 4
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 7
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.017612 s (model generation: 0.013649,  model checking: 0.003963):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<nil>() -> q_gen_291
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 5
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 5
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 5
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 5
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 10
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.019391 s (model generation: 0.014361,  model checking: 0.005030):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<nil>() -> q_gen_291
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 6
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 6
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 6
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 6
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 13
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.020992 s (model generation: 0.015541,  model checking: 0.005451):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<nil>() -> q_gen_291
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<a, b, a>() -> q_gen_293
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 9
() -> leq([z, z]) -> 7
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 7
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 7
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 16
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.023261 s (model generation: 0.018167,  model checking: 0.005094):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<nil>() -> q_gen_291
<a>() -> q_gen_292
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<a, b, a>() -> q_gen_293
<b, a, b>() -> q_gen_293
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 8
() -> leq([z, s(nn2)]) -> 10
() -> leq([z, z]) -> 8
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 8
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 8
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 19
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.024355 s (model generation: 0.019835,  model checking: 0.004520):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<nil>() -> q_gen_291
<a>() -> q_gen_292
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<a, a, a>() -> q_gen_293
<a, b, a>() -> q_gen_293
<b, a, b>() -> q_gen_293
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 9
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 9
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 9
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 9
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 22
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.036861 s (model generation: 0.023155,  model checking: 0.013706):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<cons>(q_gen_292, q_gen_291) -> q_gen_291
<nil>() -> q_gen_291
<a>() -> q_gen_292
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<a, a, a>() -> q_gen_293
<a, b, a>() -> q_gen_293
<b, a, b>() -> q_gen_293
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> length([nil, z]) -> 10
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 10
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 10
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 10
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 25
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.043788 s (model generation: 0.028401,  model checking: 0.015387):

Model:
|_
{
append -> 
{{{
Q={q_gen_274, q_gen_279, q_gen_280, q_gen_291, q_gen_292, q_gen_293},
Q_f={q_gen_274},
Delta=
{
<cons>(q_gen_292, q_gen_291) -> q_gen_291
<nil>() -> q_gen_291
<a>() -> q_gen_292
<b>() -> q_gen_292
<cons, cons>(q_gen_280, q_gen_279) -> q_gen_279
<nil, cons>(q_gen_292, q_gen_291) -> q_gen_279
<nil, nil>() -> q_gen_279
<a, a>() -> q_gen_280
<b, a>() -> q_gen_280
<b, b>() -> q_gen_280
<cons, cons, cons>(q_gen_293, q_gen_274) -> q_gen_274
<cons, nil, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, cons, cons>(q_gen_280, q_gen_279) -> q_gen_274
<nil, nil, cons>(q_gen_292, q_gen_291) -> q_gen_274
<nil, nil, nil>() -> q_gen_274
<a, a, a>() -> q_gen_293
<a, b, a>() -> q_gen_293
<b, a, b>() -> q_gen_293
<b, b, b>() -> q_gen_293
}

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

Datatype: <eltlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_270, q_gen_272},
Q_f={q_gen_270},
Delta=
{
<s>(q_gen_272) -> q_gen_272
<z>() -> q_gen_272
<s, s>(q_gen_270) -> q_gen_270
<z, s>(q_gen_272) -> q_gen_270
<z, z>() -> q_gen_270
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 11
() -> leq([z, s(nn2)]) -> 13
() -> leq([z, z]) -> 11
(append([l1, l2, _ua]) /\ length([_ua, _va]) /\ length([l1, _ta])) -> leq([_ta, _va]) -> 11
(append([l1, l2, _xa]) /\ length([_xa, _ya]) /\ length([l2, _wa])) -> leq([_wa, _ya]) -> 11
(append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]) -> 28
(length([ll, _pa])) -> length([cons(x, ll), s(_pa)]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _ka])) -> append([cons(h1, t1), l2, cons(h1, _ka)]), {
_ka -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

Total time: 0.385935
Reason for stopping: Proved