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, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)])}
(append([_n, _o, _p]) /\ append([_n, _o, _q])) -> eq_eltlist([_p, _q])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

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


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, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 0
(append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 0.308848 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_100, q_gen_101, q_gen_60, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<cons>(q_gen_76, q_gen_75) -> q_gen_75
<nil>() -> q_gen_75
<a>() -> q_gen_76
<b>() -> q_gen_76
<cons, cons>(q_gen_101, q_gen_100) -> q_gen_100
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_100
<nil, nil>() -> q_gen_100
<a, a>() -> q_gen_101
<a, b>() -> q_gen_101
<b, a>() -> q_gen_101
<b, b>() -> q_gen_101
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_101, q_gen_100) -> q_gen_60
<nil, cons, cons>(q_gen_101, q_gen_100) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<a, a, a>() -> q_gen_77
<a, b, a>() -> q_gen_77
<b, a, b>() -> q_gen_77
<b, b, b>() -> q_gen_77
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010581 s (model generation: 0.010197,  model checking: 0.000384):

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

-------------------------------------------
Step 1, which took 0.011169 s (model generation: 0.010871,  model checking: 0.000298):

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

}

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

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

-------------------------------------------
Step 2, which took 0.011153 s (model generation: 0.011082,  model checking: 0.000071):

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

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

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

})

-------------------------------------------
Step 3, which took 0.011457 s (model generation: 0.011022,  model checking: 0.000435):

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

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

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

-------------------------------------------
Step 4, which took 0.011973 s (model generation: 0.011130,  model checking: 0.000843):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63},
Q_f={q_gen_60},
Delta=
{
<nil, nil>() -> q_gen_62
<b, b>() -> q_gen_63
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
}

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

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

-------------------------------------------
Step 5, which took 0.011985 s (model generation: 0.011321,  model checking: 0.000664):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63},
Q_f={q_gen_60},
Delta=
{
<nil, nil>() -> q_gen_62
<b, b>() -> q_gen_63
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
}

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

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

-------------------------------------------
Step 6, which took 0.011837 s (model generation: 0.011547,  model checking: 0.000290):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63},
Q_f={q_gen_60},
Delta=
{
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
}

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

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

-------------------------------------------
Step 7, which took 0.014494 s (model generation: 0.012815,  model checking: 0.001679):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63},
Q_f={q_gen_60},
Delta=
{
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
}

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

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

-------------------------------------------
Step 8, which took 0.015798 s (model generation: 0.013940,  model checking: 0.001858):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<nil>() -> q_gen_75
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<b, b, b>() -> q_gen_77
}

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

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

-------------------------------------------
Step 9, which took 0.017332 s (model generation: 0.014696,  model checking: 0.002636):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<nil>() -> q_gen_75
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<b, b, b>() -> q_gen_77
}

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

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

-------------------------------------------
Step 10, which took 0.018698 s (model generation: 0.015580,  model checking: 0.003118):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<nil>() -> q_gen_75
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<a, b, a>() -> q_gen_77
<b, b, b>() -> q_gen_77
}

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

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

-------------------------------------------
Step 11, which took 0.020606 s (model generation: 0.018199,  model checking: 0.002407):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<nil>() -> q_gen_75
<a>() -> q_gen_76
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<a, b, a>() -> q_gen_77
<b, a, b>() -> q_gen_77
<b, b, b>() -> q_gen_77
}

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

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

-------------------------------------------
Step 12, which took 0.022656 s (model generation: 0.019608,  model checking: 0.003048):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<nil>() -> q_gen_75
<a>() -> q_gen_76
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<a, a, a>() -> q_gen_77
<a, b, a>() -> q_gen_77
<b, a, b>() -> q_gen_77
<b, b, b>() -> q_gen_77
}

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

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

-------------------------------------------
Step 13, which took 0.032636 s (model generation: 0.023719,  model checking: 0.008917):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<cons>(q_gen_76, q_gen_75) -> q_gen_75
<nil>() -> q_gen_75
<a>() -> q_gen_76
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<a, a, a>() -> q_gen_77
<a, b, a>() -> q_gen_77
<b, a, b>() -> q_gen_77
<b, b, b>() -> q_gen_77
}

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

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

-------------------------------------------
Step 14, which took 0.038194 s (model generation: 0.029202,  model checking: 0.008992):

Model:
|_
{
append -> 
{{{
Q={q_gen_60, q_gen_62, q_gen_63, q_gen_75, q_gen_76, q_gen_77},
Q_f={q_gen_60},
Delta=
{
<cons>(q_gen_76, q_gen_75) -> q_gen_75
<nil>() -> q_gen_75
<a>() -> q_gen_76
<b>() -> q_gen_76
<cons, cons>(q_gen_63, q_gen_62) -> q_gen_62
<nil, cons>(q_gen_76, q_gen_75) -> q_gen_62
<nil, nil>() -> q_gen_62
<a, a>() -> q_gen_63
<b, a>() -> q_gen_63
<b, b>() -> q_gen_63
<cons, cons, cons>(q_gen_77, q_gen_60) -> q_gen_60
<cons, nil, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, cons, cons>(q_gen_63, q_gen_62) -> q_gen_60
<nil, nil, cons>(q_gen_76, q_gen_75) -> q_gen_60
<nil, nil, nil>() -> q_gen_60
<a, a, a>() -> q_gen_77
<a, b, a>() -> q_gen_77
<b, a, b>() -> q_gen_77
<b, b, b>() -> q_gen_77
}

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

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

Total time: 0.308848
Reason for stopping: Proved