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, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)])}
(append([_ek, _fk, _gk]) /\ append([_ek, _fk, _hk])) -> eq_eltlist([_gk, _hk])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

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


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
(append([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 0
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 0
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 0.260666 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<cons>(q_gen_2626, q_gen_2625) -> q_gen_2625
<nil>() -> q_gen_2625
<a>() -> q_gen_2626
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<a, b>() -> q_gen_2616
<b, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<a, a, a>() -> q_gen_2627
<a, b, a>() -> q_gen_2627
<b, a, b>() -> q_gen_2627
<b, b, b>() -> q_gen_2627
}

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

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010886 s (model generation: 0.010586,  model checking: 0.000300):

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

-------------------------------------------
Step 1, which took 0.009984 s (model generation: 0.009819,  model checking: 0.000165):

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

}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 1
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 1
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.007796 s (model generation: 0.007782,  model checking: 0.000014):

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

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 1
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 1
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.007884 s (model generation: 0.007715,  model checking: 0.000169):

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

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 1
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 1
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.007823 s (model generation: 0.007587,  model checking: 0.000236):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616},
Q_f={q_gen_2613},
Delta=
{
<nil, nil>() -> q_gen_2615
<b, b>() -> q_gen_2616
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 2
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 2
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> a
})

-------------------------------------------
Step 5, which took 0.009268 s (model generation: 0.008704,  model checking: 0.000564):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616},
Q_f={q_gen_2613},
Delta=
{
<nil, nil>() -> q_gen_2615
<b, b>() -> q_gen_2616
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 3
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 3
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 6, which took 0.010010 s (model generation: 0.008917,  model checking: 0.001093):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616},
Q_f={q_gen_2613},
Delta=
{
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
}

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

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

-------------------------------------------
Step 7, which took 0.010477 s (model generation: 0.010013,  model checking: 0.000464):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<b, b, b>() -> q_gen_2627
}

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

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

-------------------------------------------
Step 8, which took 0.011145 s (model generation: 0.010914,  model checking: 0.000231):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 7
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 7
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 7
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]), {
_ik -> cons(b, cons(b, nil))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.013008 s (model generation: 0.011807,  model checking: 0.001201):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 7
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 7
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 10
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.013819 s (model generation: 0.012151,  model checking: 0.001668):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 8
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 8
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 13
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.015006 s (model generation: 0.013025,  model checking: 0.001981):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<a, b, a>() -> q_gen_2627
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 9
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 9
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 16
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.017094 s (model generation: 0.015709,  model checking: 0.001385):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<a>() -> q_gen_2626
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<a, b, a>() -> q_gen_2627
<b, a, b>() -> q_gen_2627
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 10
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 10
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 19
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.018383 s (model generation: 0.016722,  model checking: 0.001661):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<nil>() -> q_gen_2625
<a>() -> q_gen_2626
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<a, a, a>() -> q_gen_2627
<a, b, a>() -> q_gen_2627
<b, a, b>() -> q_gen_2627
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 11
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 11
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 22
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.025244 s (model generation: 0.020332,  model checking: 0.004912):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<cons>(q_gen_2626, q_gen_2625) -> q_gen_2625
<nil>() -> q_gen_2625
<a>() -> q_gen_2626
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<a, a, a>() -> q_gen_2627
<a, b, a>() -> q_gen_2627
<b, a, b>() -> q_gen_2627
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 12
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 12
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 25
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.030347 s (model generation: 0.024830,  model checking: 0.005517):

Model:
|_
{
append -> 
{{{
Q={q_gen_2613, q_gen_2615, q_gen_2616, q_gen_2625, q_gen_2626, q_gen_2627},
Q_f={q_gen_2613},
Delta=
{
<cons>(q_gen_2626, q_gen_2625) -> q_gen_2625
<nil>() -> q_gen_2625
<a>() -> q_gen_2626
<b>() -> q_gen_2626
<cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2615
<nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2615
<nil, nil>() -> q_gen_2615
<a, a>() -> q_gen_2616
<b, a>() -> q_gen_2616
<b, b>() -> q_gen_2616
<cons, cons, cons>(q_gen_2627, q_gen_2613) -> q_gen_2613
<cons, nil, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, cons, cons>(q_gen_2616, q_gen_2615) -> q_gen_2613
<nil, nil, cons>(q_gen_2626, q_gen_2625) -> q_gen_2613
<nil, nil, nil>() -> q_gen_2613
<a, a, a>() -> q_gen_2627
<a, b, a>() -> q_gen_2627
<b, a, b>() -> q_gen_2627
<b, b, b>() -> q_gen_2627
}

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

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([l1, l2, _ik]) /\ not_null([l1])) -> not_null([_ik]) -> 13
(append([l1, l2, _jk]) /\ not_null([l2])) -> not_null([_jk]) -> 13
(append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]) -> 28
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _dk])) -> append([cons(h1, t1), l2, cons(h1, _dk)]), {
_dk -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

Total time: 0.260666
Reason for stopping: Proved