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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)])}
(append([_jg, _kg, _lg]) /\ append([_jg, _kg, _mg])) -> eq_eltlist([_lg, _mg])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(append([cons(i, l1), l2, _ng])) -> not_null([_ng])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
(append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 0
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 0.225041 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<cons>(q_gen_1594, q_gen_1593) -> q_gen_1593
<nil>() -> q_gen_1593
<a>() -> q_gen_1594
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<a, b>() -> q_gen_1581
<b, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<a, a, a>() -> q_gen_1595
<a, b, a>() -> q_gen_1595
<b, a, b>() -> q_gen_1595
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007740 s (model generation: 0.007569,  model checking: 0.000171):

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

}

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

}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 1
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> b
})

-------------------------------------------
Step 1, which took 0.007668 s (model generation: 0.007538,  model checking: 0.000130):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<nil>() -> q_gen_1575
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 1
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.008766 s (model generation: 0.008751,  model checking: 0.000015):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<nil>() -> q_gen_1575
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 1
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.008475 s (model generation: 0.008274,  model checking: 0.000201):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 4
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 2
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.008041 s (model generation: 0.007771,  model checking: 0.000270):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581},
Q_f={q_gen_1578},
Delta=
{
<nil, nil>() -> q_gen_1580
<b, b>() -> q_gen_1581
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 4
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 3
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> a
})

-------------------------------------------
Step 5, which took 0.009179 s (model generation: 0.007924,  model checking: 0.001255):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581},
Q_f={q_gen_1578},
Delta=
{
<nil, nil>() -> q_gen_1580
<b, b>() -> q_gen_1581
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 4
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.009524 s (model generation: 0.009384,  model checking: 0.000140):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581},
Q_f={q_gen_1578},
Delta=
{
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 4
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 7
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([cons(i, l1), l2, _ng])) -> not_null([_ng]), {
_ng -> cons(b, cons(b, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 7, which took 0.010531 s (model generation: 0.009063,  model checking: 0.001468):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581},
Q_f={q_gen_1578},
Delta=
{
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 7
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 7
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.011498 s (model generation: 0.010326,  model checking: 0.001172):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<nil>() -> q_gen_1593
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 10
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 8
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.012386 s (model generation: 0.010909,  model checking: 0.001477):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<nil>() -> q_gen_1593
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 13
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 9
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.017448 s (model generation: 0.015877,  model checking: 0.001571):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<nil>() -> q_gen_1593
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<a, b, a>() -> q_gen_1595
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 16
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 10
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.015383 s (model generation: 0.014024,  model checking: 0.001359):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<nil>() -> q_gen_1593
<a>() -> q_gen_1594
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<a, b, a>() -> q_gen_1595
<b, a, b>() -> q_gen_1595
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 19
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 11
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.016218 s (model generation: 0.014322,  model checking: 0.001896):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<nil>() -> q_gen_1593
<a>() -> q_gen_1594
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<a, a, a>() -> q_gen_1595
<a, b, a>() -> q_gen_1595
<b, a, b>() -> q_gen_1595
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 22
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 12
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.021260 s (model generation: 0.017272,  model checking: 0.003988):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<cons>(q_gen_1594, q_gen_1593) -> q_gen_1593
<nil>() -> q_gen_1593
<a>() -> q_gen_1594
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<a, a, a>() -> q_gen_1595
<a, b, a>() -> q_gen_1595
<b, a, b>() -> q_gen_1595
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 25
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 13
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.026585 s (model generation: 0.022289,  model checking: 0.004296):

Model:
|_
{
append -> 
{{{
Q={q_gen_1578, q_gen_1580, q_gen_1581, q_gen_1593, q_gen_1594, q_gen_1595},
Q_f={q_gen_1578},
Delta=
{
<cons>(q_gen_1594, q_gen_1593) -> q_gen_1593
<nil>() -> q_gen_1593
<a>() -> q_gen_1594
<b>() -> q_gen_1594
<cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1580
<nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1580
<nil, nil>() -> q_gen_1580
<a, a>() -> q_gen_1581
<b, a>() -> q_gen_1581
<b, b>() -> q_gen_1581
<cons, cons, cons>(q_gen_1595, q_gen_1578) -> q_gen_1578
<cons, nil, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, cons, cons>(q_gen_1581, q_gen_1580) -> q_gen_1578
<nil, nil, cons>(q_gen_1594, q_gen_1593) -> q_gen_1578
<nil, nil, nil>() -> q_gen_1578
<a, a, a>() -> q_gen_1595
<a, b, a>() -> q_gen_1595
<b, a, b>() -> q_gen_1595
<b, b, b>() -> q_gen_1595
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_1575, q_gen_1576, q_gen_1577},
Q_f={q_gen_1575},
Delta=
{
<cons>(q_gen_1577, q_gen_1575) -> q_gen_1575
<cons>(q_gen_1577, q_gen_1576) -> q_gen_1575
<nil>() -> q_gen_1576
<a>() -> q_gen_1577
<b>() -> q_gen_1577
}

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

}
--
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([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]) -> 28
(append([cons(i, l1), l2, _ng])) -> not_null([_ng]) -> 14
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _ig])) -> append([cons(h1, t1), l2, cons(h1, _ig)]), {
_ig -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

Total time: 0.225041
Reason for stopping: Proved