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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)])}
(append([_kq, _lq, _mq]) /\ append([_kq, _lq, _nq])) -> eq_eltlist([_mq, _nq])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]), (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq])}


over-approximation: {append}
under-approximation: {}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 0
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 0
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 0.153591 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<cons>(q_gen_3185, q_gen_3184) -> q_gen_3184
<nil>() -> q_gen_3184
<a>() -> q_gen_3185
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<a, b>() -> q_gen_3175
<b, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<a, a, a>() -> q_gen_3186
<a, b, a>() -> q_gen_3186
<b, a, b>() -> q_gen_3186
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007046 s (model generation: 0.005542,  model checking: 0.001504):

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

}

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

}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 3
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 1
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 1
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> b
})

-------------------------------------------
Step 1, which took 0.005101 s (model generation: 0.004716,  model checking: 0.000385):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<nil>() -> q_gen_3169
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 1
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 1
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.005168 s (model generation: 0.005148,  model checking: 0.000020):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<nil>() -> q_gen_3169
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 1
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 1
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.005169 s (model generation: 0.004519,  model checking: 0.000650):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 1
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 1
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.005546 s (model generation: 0.004915,  model checking: 0.000631):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175},
Q_f={q_gen_3172},
Delta=
{
<nil, nil>() -> q_gen_3174
<b, b>() -> q_gen_3175
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 6
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 2
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 2
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> a
})

-------------------------------------------
Step 5, which took 0.006797 s (model generation: 0.006397,  model checking: 0.000400):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175},
Q_f={q_gen_3172},
Delta=
{
<nil, nil>() -> q_gen_3174
<b, b>() -> q_gen_3175
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 3
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 3
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.006140 s (model generation: 0.004921,  model checking: 0.001219):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175},
Q_f={q_gen_3172},
Delta=
{
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 4
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 4
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 7
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.006544 s (model generation: 0.006101,  model checking: 0.000443):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<nil>() -> q_gen_3184
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 4
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 7
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 7
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]), {
_pq -> cons(b, cons(b, nil))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 8, which took 0.007444 s (model generation: 0.006491,  model checking: 0.000953):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<nil>() -> q_gen_3184
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> not_null([cons(x, ll)]) -> 7
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 5
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 7
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 10
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.008610 s (model generation: 0.006575,  model checking: 0.002035):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<nil>() -> q_gen_3184
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> not_null([cons(x, ll)]) -> 8
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 6
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 8
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 13
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.008537 s (model generation: 0.007146,  model checking: 0.001391):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<nil>() -> q_gen_3184
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<a, b, a>() -> q_gen_3186
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> not_null([cons(x, ll)]) -> 9
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 7
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 9
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 16
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.010377 s (model generation: 0.007977,  model checking: 0.002400):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<nil>() -> q_gen_3184
<a>() -> q_gen_3185
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<a, b, a>() -> q_gen_3186
<b, a, b>() -> q_gen_3186
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> not_null([cons(x, ll)]) -> 10
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 8
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 10
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 19
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.011238 s (model generation: 0.009186,  model checking: 0.002052):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<nil>() -> q_gen_3184
<a>() -> q_gen_3185
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<a, a, a>() -> q_gen_3186
<a, b, a>() -> q_gen_3186
<b, a, b>() -> q_gen_3186
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> not_null([cons(x, ll)]) -> 11
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 9
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 11
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 22
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.014177 s (model generation: 0.010710,  model checking: 0.003467):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<cons>(q_gen_3185, q_gen_3184) -> q_gen_3184
<nil>() -> q_gen_3184
<a>() -> q_gen_3185
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<a, a, a>() -> q_gen_3186
<a, b, a>() -> q_gen_3186
<b, a, b>() -> q_gen_3186
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> not_null([cons(x, ll)]) -> 12
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 10
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 12
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 25
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.017791 s (model generation: 0.013144,  model checking: 0.004647):

Model:
|_
{
append -> 
{{{
Q={q_gen_3172, q_gen_3174, q_gen_3175, q_gen_3184, q_gen_3185, q_gen_3186},
Q_f={q_gen_3172},
Delta=
{
<cons>(q_gen_3185, q_gen_3184) -> q_gen_3184
<nil>() -> q_gen_3184
<a>() -> q_gen_3185
<b>() -> q_gen_3185
<cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3174
<nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3174
<nil, nil>() -> q_gen_3174
<a, a>() -> q_gen_3175
<b, a>() -> q_gen_3175
<b, b>() -> q_gen_3175
<cons, cons, cons>(q_gen_3186, q_gen_3172) -> q_gen_3172
<cons, nil, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, cons, cons>(q_gen_3175, q_gen_3174) -> q_gen_3172
<nil, nil, cons>(q_gen_3185, q_gen_3184) -> q_gen_3172
<nil, nil, nil>() -> q_gen_3172
<a, a, a>() -> q_gen_3186
<a, b, a>() -> q_gen_3186
<b, a, b>() -> q_gen_3186
<b, b, b>() -> q_gen_3186
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_3169, q_gen_3170, q_gen_3171},
Q_f={q_gen_3169},
Delta=
{
<cons>(q_gen_3171, q_gen_3169) -> q_gen_3169
<cons>(q_gen_3171, q_gen_3170) -> q_gen_3169
<nil>() -> q_gen_3170
<a>() -> q_gen_3171
<b>() -> q_gen_3171
}

Datatype: <eltlist>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> not_null([cons(x, ll)]) -> 13
(append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 11
(append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 13
(append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 28
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

Total time: 0.153591
Reason for stopping: Proved