Solving ../../benchmarks/true/append_not_null3.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


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 30.001800 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_784, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_791, q_gen_792, q_gen_793, q_gen_794, q_gen_795, q_gen_796, q_gen_797, q_gen_798, q_gen_799, q_gen_800, q_gen_801, q_gen_803, q_gen_804, q_gen_805, q_gen_806, q_gen_807, q_gen_808, q_gen_809, q_gen_810, q_gen_811, q_gen_812, q_gen_813, q_gen_814, q_gen_815, q_gen_816, q_gen_817, q_gen_818, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825, q_gen_826, q_gen_827, q_gen_828, q_gen_829, q_gen_830, q_gen_831, q_gen_832, q_gen_833, q_gen_834, q_gen_835, q_gen_836, q_gen_837, q_gen_838, q_gen_839, q_gen_840, q_gen_841, q_gen_842, q_gen_843, q_gen_844, q_gen_845, q_gen_846, q_gen_847, q_gen_848, q_gen_849, q_gen_850, q_gen_851, q_gen_852, q_gen_853, q_gen_854, q_gen_855, q_gen_856, q_gen_857, q_gen_858, q_gen_859, q_gen_860, q_gen_861, q_gen_862, q_gen_863, q_gen_864, q_gen_865, q_gen_866, q_gen_867, q_gen_868, q_gen_869, q_gen_870, q_gen_871, q_gen_872, q_gen_873, q_gen_874, q_gen_875, q_gen_876, q_gen_877, q_gen_878, q_gen_879, q_gen_880, q_gen_881, q_gen_882, q_gen_883, q_gen_884, q_gen_885, q_gen_886, q_gen_887, q_gen_888, q_gen_889, q_gen_890, q_gen_891, q_gen_892, q_gen_893, q_gen_894, q_gen_895, q_gen_896, q_gen_897, q_gen_898, q_gen_899, q_gen_900},
Q_f={},
Delta=
{
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_806
<cons>(q_gen_806, q_gen_799) -> q_gen_814
<cons>(q_gen_800, q_gen_799) -> q_gen_854
<nil, nil>() -> q_gen_785
<nil, b>() -> q_gen_786
<b, nil>() -> q_gen_787
<b, b>() -> q_gen_788
<nil, a>() -> q_gen_792
<a, nil>() -> q_gen_793
<a, a>() -> q_gen_794
<cons, cons>(q_gen_794, q_gen_793, q_gen_792, q_gen_785) -> q_gen_797
<cons, b>(q_gen_800, q_gen_799) -> q_gen_798
<b, cons>(q_gen_800, q_gen_799) -> q_gen_801
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_804
<cons, b>(q_gen_806, q_gen_799) -> q_gen_805
<b, cons>(q_gen_806, q_gen_799) -> q_gen_807
<cons, a>(q_gen_806, q_gen_799) -> q_gen_809
<a, cons>(q_gen_806, q_gen_799) -> q_gen_810
<cons, cons>(q_gen_788, q_gen_807, q_gen_805, q_gen_804) -> q_gen_812
<cons, b>(q_gen_806, q_gen_814) -> q_gen_813
<b, cons>(q_gen_806, q_gen_814) -> q_gen_815
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_828
<a, cons>(q_gen_800, q_gen_799) -> q_gen_850
<a, b>() -> q_gen_851
<nil, cons>(q_gen_806, q_gen_799) -> q_gen_861
<b, a>() -> q_gen_862
<nil, nil, nil>() -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_784
<nil, cons, cons>(q_gen_794, q_gen_793, q_gen_792, q_gen_785) -> q_gen_791
<cons, nil, cons>(q_gen_794, q_gen_793, q_gen_792, q_gen_785) -> q_gen_795
<cons, nil, cons>(q_gen_788, q_gen_801, q_gen_798, q_gen_797) -> q_gen_796
<nil, cons, cons>(q_gen_788, q_gen_807, q_gen_805, q_gen_804) -> q_gen_803
<cons, nil, cons>(q_gen_794, q_gen_810, q_gen_809, q_gen_804) -> q_gen_808
<nil, cons, cons>(q_gen_788, q_gen_815, q_gen_813, q_gen_812) -> q_gen_811
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_816
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_818) -> q_gen_817
<nil, nil, cons>(q_gen_806, q_gen_799) -> q_gen_818
<nil, nil, b>() -> q_gen_819
<nil, b, cons>(q_gen_806, q_gen_799) -> q_gen_820
<nil, b, b>() -> q_gen_821
<b, nil, cons>(q_gen_806, q_gen_799) -> q_gen_822
<b, nil, b>() -> q_gen_823
<b, b, cons>(q_gen_806, q_gen_799) -> q_gen_824
<b, b, b>() -> q_gen_825
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_826
<cons, nil, cons>(q_gen_788, q_gen_801, q_gen_786, q_gen_828) -> q_gen_827
<cons, cons, cons>(q_gen_834, q_gen_833, q_gen_823, q_gen_832, q_gen_831, q_gen_830, q_gen_819, q_gen_826) -> q_gen_829
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_830
<nil, a, b>() -> q_gen_831
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_832
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_833
<b, a, b>() -> q_gen_834
<cons, cons, cons>(q_gen_841, q_gen_840, q_gen_839, q_gen_838, q_gen_837, q_gen_820, q_gen_836, q_gen_818) -> q_gen_835
<nil, nil, a>() -> q_gen_836
<nil, b, a>() -> q_gen_837
<a, nil, cons>(q_gen_806, q_gen_799) -> q_gen_838
<a, nil, a>() -> q_gen_839
<a, b, cons>(q_gen_806, q_gen_799) -> q_gen_840
<a, b, a>() -> q_gen_841
<cons, cons, cons>(q_gen_846, q_gen_845, q_gen_839, q_gen_844, q_gen_843, q_gen_830, q_gen_836, q_gen_826) -> q_gen_842
<nil, a, a>() -> q_gen_843
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_844
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_845
<a, a, a>() -> q_gen_846
<nil, cons, cons>(q_gen_788, q_gen_801, q_gen_798, q_gen_797) -> q_gen_847
<cons, cons, cons>(q_gen_825, q_gen_857, q_gen_856, q_gen_855, q_gen_821, q_gen_853, q_gen_852, q_gen_849) -> q_gen_848
<nil, cons, cons>(q_gen_851, q_gen_850, q_gen_786, q_gen_828) -> q_gen_849
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_852
<nil, b, cons>(q_gen_806, q_gen_854) -> q_gen_853
<b, cons, cons>(q_gen_851, q_gen_850, q_gen_786, q_gen_828) -> q_gen_855
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_856
<b, b, cons>(q_gen_806, q_gen_854) -> q_gen_857
<nil, cons, cons>(q_gen_794, q_gen_810, q_gen_809, q_gen_804) -> q_gen_858
<cons, cons, cons>(q_gen_846, q_gen_867, q_gen_866, q_gen_865, q_gen_843, q_gen_864, q_gen_863, q_gen_860) -> q_gen_859
<nil, cons, cons>(q_gen_862, q_gen_807, q_gen_792, q_gen_861) -> q_gen_860
<nil, cons, a>(q_gen_806, q_gen_799) -> q_gen_863
<nil, a, cons>(q_gen_800, q_gen_814) -> q_gen_864
<a, cons, cons>(q_gen_862, q_gen_807, q_gen_792, q_gen_861) -> q_gen_865
<a, cons, a>(q_gen_806, q_gen_799) -> q_gen_866
<a, a, cons>(q_gen_800, q_gen_814) -> q_gen_867
<cons, cons, cons>(q_gen_825, q_gen_874, q_gen_823, q_gen_873, q_gen_872, q_gen_871, q_gen_870, q_gen_869) -> q_gen_868
<cons, nil, cons>(q_gen_788, q_gen_807, q_gen_786, q_gen_861) -> q_gen_869
<cons, nil, b>(q_gen_806, q_gen_799) -> q_gen_870
<cons, b, cons>(q_gen_788, q_gen_807, q_gen_786, q_gen_861) -> q_gen_871
<cons, b, b>(q_gen_806, q_gen_799) -> q_gen_872
<b, nil, cons>(q_gen_806, q_gen_814) -> q_gen_873
<b, b, cons>(q_gen_806, q_gen_814) -> q_gen_874
<cons, cons, cons>(q_gen_834, q_gen_877, q_gen_823, q_gen_822, q_gen_831, q_gen_876, q_gen_819, q_gen_818) -> q_gen_875
<nil, a, cons>(q_gen_806, q_gen_799) -> q_gen_876
<b, a, cons>(q_gen_806, q_gen_799) -> q_gen_877
<cons, cons, cons>(q_gen_834, q_gen_881, q_gen_823, q_gen_873, q_gen_880, q_gen_879, q_gen_870, q_gen_869) -> q_gen_878
<cons, a, cons>(q_gen_788, q_gen_807, q_gen_786, q_gen_861) -> q_gen_879
<cons, a, b>(q_gen_806, q_gen_799) -> q_gen_880
<b, a, cons>(q_gen_806, q_gen_814) -> q_gen_881
<cons, cons, cons>(q_gen_841, q_gen_886, q_gen_839, q_gen_885, q_gen_884, q_gen_871, q_gen_883, q_gen_869) -> q_gen_882
<cons, nil, a>(q_gen_806, q_gen_799) -> q_gen_883
<cons, b, a>(q_gen_806, q_gen_799) -> q_gen_884
<a, nil, cons>(q_gen_806, q_gen_814) -> q_gen_885
<a, b, cons>(q_gen_806, q_gen_814) -> q_gen_886
<cons, cons, cons>(q_gen_846, q_gen_889, q_gen_839, q_gen_885, q_gen_888, q_gen_879, q_gen_883, q_gen_869) -> q_gen_887
<cons, a, a>(q_gen_806, q_gen_799) -> q_gen_888
<a, a, cons>(q_gen_806, q_gen_814) -> q_gen_889
<cons, cons, cons>(q_gen_834, q_gen_877, q_gen_893, q_gen_892, q_gen_831, q_gen_876, q_gen_891, q_gen_816) -> q_gen_890
<nil, cons, b>(q_gen_806, q_gen_799) -> q_gen_891
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_892
<b, cons, b>(q_gen_806, q_gen_799) -> q_gen_893
<cons, cons, cons>(q_gen_834, q_gen_881, q_gen_893, q_gen_896, q_gen_880, q_gen_879, q_gen_895, q_gen_817) -> q_gen_894
<cons, cons, b>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_895
<b, cons, cons>(q_gen_788, q_gen_807, q_gen_786, q_gen_861) -> q_gen_896
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_893, q_gen_892, q_gen_821, q_gen_820, q_gen_891, q_gen_816) -> q_gen_897
<cons, cons, cons>(q_gen_841, q_gen_886, q_gen_866, q_gen_900, q_gen_884, q_gen_871, q_gen_899, q_gen_817) -> q_gen_898
<cons, cons, a>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_899
<a, cons, cons>(q_gen_788, q_gen_807, q_gen_786, q_gen_861) -> q_gen_900
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782, q_gen_789, q_gen_790, q_gen_802},
Q_f={},
Delta=
{
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<b>() -> q_gen_782
<cons>(q_gen_790, q_gen_781) -> q_gen_789
<a>() -> q_gen_790
<cons>(q_gen_782, q_gen_789) -> q_gen_802
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004503 s (model generation: 0.003946,  model checking: 0.000557):

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

}

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

}

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

}
--
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: Yes: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> b
})

-------------------------------------------
Step 1, which took 0.004096 s (model generation: 0.003581,  model checking: 0.000515):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<nil>() -> q_gen_780
<b>() -> q_gen_782
}

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

}
--
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: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.003542 s (model generation: 0.003534,  model checking: 0.000008):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<nil>() -> q_gen_780
<b>() -> q_gen_782
}

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

}
--
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: Yes: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.003793 s (model generation: 0.003437,  model checking: 0.000356):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<b>() -> q_gen_782
}

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

}
--
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: Yes: ((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.004796 s (model generation: 0.003828,  model checking: 0.000968):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788},
Q_f={q_gen_783},
Delta=
{
<nil, nil>() -> q_gen_785
<nil, b>() -> q_gen_786
<b, nil>() -> q_gen_787
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<b>() -> q_gen_782
}

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

}
--
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: Yes: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> a
})

-------------------------------------------
Step 5, which took 0.007590 s (model generation: 0.005462,  model checking: 0.002128):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788},
Q_f={q_gen_783},
Delta=
{
<nil, nil>() -> q_gen_785
<nil, b>() -> q_gen_786
<b, nil>() -> q_gen_787
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

}
--
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: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 6, which took 0.009328 s (model generation: 0.005397,  model checking: 0.003931):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788},
Q_f={q_gen_783},
Delta=
{
<nil, nil>() -> q_gen_785
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, nil>() -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

-------------------------------------------
Step 7, which took 0.005218 s (model generation: 0.004882,  model checking: 0.000336):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800},
Q_f={q_gen_783},
Delta=
{
<nil>() -> q_gen_799
<a>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

-------------------------------------------
Step 8, which took 0.014710 s (model generation: 0.005054,  model checking: 0.009656):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800},
Q_f={q_gen_783},
Delta=
{
<nil>() -> q_gen_799
<a>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

-------------------------------------------
Step 9, which took 0.010043 s (model generation: 0.005488,  model checking: 0.004555):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800},
Q_f={q_gen_783},
Delta=
{
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

}
--
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)]) -> 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 -> 8
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.013201 s (model generation: 0.005517,  model checking: 0.007684):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800},
Q_f={q_gen_783},
Delta=
{
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

-------------------------------------------
Step 11, which took 0.009677 s (model generation: 0.005950,  model checking: 0.003727):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

}
--
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)]) -> 9  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 13  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 10  ;  (not_null([nil])) -> BOT -> 10
}
Sat witness: Yes: ((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 12, which took 0.034548 s (model generation: 0.007162,  model checking: 0.027386):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, nil, b>() -> q_gen_819
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, b>() -> q_gen_821
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, nil, b>() -> q_gen_823
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

-------------------------------------------
Step 13, which took 0.078041 s (model generation: 0.008864,  model checking: 0.069177):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, nil, b>() -> q_gen_819
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, b>() -> q_gen_821
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, nil, b>() -> q_gen_823
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> not_null([cons(x, ll)]) -> 11  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 19  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 12  ;  (not_null([nil])) -> BOT -> 12
}
Sat witness: Yes: ((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 14, which took 0.208162 s (model generation: 0.009700,  model checking: 0.198462):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, nil, b>() -> q_gen_819
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, a, b>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, nil, b>() -> q_gen_823
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> not_null([cons(x, ll)]) -> 12  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 22  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 13  ;  (not_null([nil])) -> BOT -> 13
}
Sat witness: Yes: ((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 15, which took 0.071393 s (model generation: 0.010683,  model checking: 0.060710):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, nil, a>() -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> not_null([cons(x, ll)]) -> 13  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 25  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 14  ;  (not_null([nil])) -> BOT -> 14
}
Sat witness: Yes: ((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 16, which took 1.222127 s (model generation: 0.011728,  model checking: 1.210399):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, nil, a>() -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> not_null([cons(x, ll)]) -> 14  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 28  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 15  ;  (not_null([nil])) -> BOT -> 15
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.541336 s (model generation: 0.014488,  model checking: 0.526848):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> not_null([cons(x, ll)]) -> 15  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 31  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 16  ;  (not_null([nil])) -> BOT -> 16
}
Sat witness: Yes: ((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 18, which took 3.389480 s (model generation: 0.017097,  model checking: 3.372383):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<nil, cons, a>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, cons, a>(q_gen_800, q_gen_799) -> q_gen_823
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> not_null([cons(x, ll)]) -> 16  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 34  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 17  ;  (not_null([nil])) -> BOT -> 17
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 1.559386 s (model generation: 0.020086,  model checking: 1.539300):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<cons, nil, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, a>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<cons, b, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<cons, b, b>(q_gen_800, q_gen_799) -> q_gen_821
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, cons, a>(q_gen_800, q_gen_799) -> q_gen_823
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> not_null([cons(x, ll)]) -> 17  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 37  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 18  ;  (not_null([nil])) -> BOT -> 18
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 20, which took 3.331080 s (model generation: 0.028044,  model checking: 3.303036):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<cons, nil, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, a>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<cons, a, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<cons, b, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<cons, a, b>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, b>(q_gen_800, q_gen_799) -> q_gen_821
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, cons, a>(q_gen_800, q_gen_799) -> q_gen_823
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> not_null([cons(x, ll)]) -> 18  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 40  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 19  ;  (not_null([nil])) -> BOT -> 19
}
Sat witness: Yes: ((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 -> cons(b, nil)
})

-------------------------------------------
Step 21, which took 3.396420 s (model generation: 0.033858,  model checking: 3.362562):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<cons, nil, a>(q_gen_800, q_gen_799) -> q_gen_819
<cons, nil, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, a>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<cons, a, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<cons, b, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<cons, a, b>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, a>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, b>(q_gen_800, q_gen_799) -> q_gen_821
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, cons, a>(q_gen_800, q_gen_799) -> q_gen_823
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> not_null([cons(x, ll)]) -> 19  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 43  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 20  ;  (not_null([nil])) -> BOT -> 20
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 22, which took 1.611710 s (model generation: 0.035874,  model checking: 1.575836):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<cons, nil, a>(q_gen_800, q_gen_799) -> q_gen_819
<cons, nil, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, a>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<cons, a, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<cons, b, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<cons, a, a>(q_gen_800, q_gen_799) -> q_gen_821
<cons, a, b>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, a>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, b>(q_gen_800, q_gen_799) -> q_gen_821
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, cons, a>(q_gen_800, q_gen_799) -> q_gen_823
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> not_null([cons(x, ll)]) -> 20  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 46  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 21  ;  (not_null([nil])) -> BOT -> 21
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 7.585906 s (model generation: 0.042279,  model checking: 7.543627):

Model:
|_
{
append -> 
{{{
Q={q_gen_783, q_gen_785, q_gen_786, q_gen_787, q_gen_788, q_gen_799, q_gen_800, q_gen_819, q_gen_820, q_gen_821, q_gen_822, q_gen_823, q_gen_824, q_gen_825},
Q_f={q_gen_783},
Delta=
{
<cons>(q_gen_800, q_gen_799) -> q_gen_799
<nil>() -> q_gen_799
<a>() -> q_gen_800
<b>() -> q_gen_800
<cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_785
<nil, cons>(q_gen_800, q_gen_799) -> q_gen_785
<nil, nil>() -> q_gen_785
<cons, a>(q_gen_800, q_gen_799) -> q_gen_786
<cons, b>(q_gen_800, q_gen_799) -> q_gen_786
<nil, a>() -> q_gen_786
<nil, b>() -> q_gen_786
<a, cons>(q_gen_800, q_gen_799) -> q_gen_787
<a, nil>() -> q_gen_787
<b, cons>(q_gen_800, q_gen_799) -> q_gen_787
<b, nil>() -> q_gen_787
<a, a>() -> q_gen_788
<a, b>() -> q_gen_788
<b, a>() -> q_gen_788
<b, b>() -> q_gen_788
<cons, cons, cons>(q_gen_825, q_gen_824, q_gen_823, q_gen_822, q_gen_821, q_gen_820, q_gen_819, q_gen_783) -> q_gen_783
<cons, nil, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_783
<nil, nil, cons>(q_gen_800, q_gen_799) -> q_gen_783
<nil, nil, nil>() -> q_gen_783
<cons, cons, b>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_819
<cons, nil, a>(q_gen_800, q_gen_799) -> q_gen_819
<cons, nil, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, a>(q_gen_800, q_gen_799) -> q_gen_819
<nil, cons, b>(q_gen_800, q_gen_799) -> q_gen_819
<nil, nil, a>() -> q_gen_819
<nil, nil, b>() -> q_gen_819
<cons, a, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<cons, b, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_820
<nil, a, cons>(q_gen_800, q_gen_799) -> q_gen_820
<nil, b, cons>(q_gen_800, q_gen_799) -> q_gen_820
<cons, a, a>(q_gen_800, q_gen_799) -> q_gen_821
<cons, a, b>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, a>(q_gen_800, q_gen_799) -> q_gen_821
<cons, b, b>(q_gen_800, q_gen_799) -> q_gen_821
<nil, a, a>() -> q_gen_821
<nil, a, b>() -> q_gen_821
<nil, b, a>() -> q_gen_821
<nil, b, b>() -> q_gen_821
<a, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<a, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<b, cons, cons>(q_gen_788, q_gen_787, q_gen_786, q_gen_785) -> q_gen_822
<b, nil, cons>(q_gen_800, q_gen_799) -> q_gen_822
<a, cons, a>(q_gen_800, q_gen_799) -> q_gen_823
<a, nil, a>() -> q_gen_823
<b, cons, b>(q_gen_800, q_gen_799) -> q_gen_823
<b, nil, b>() -> q_gen_823
<a, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, a, cons>(q_gen_800, q_gen_799) -> q_gen_824
<b, b, cons>(q_gen_800, q_gen_799) -> q_gen_824
<a, a, a>() -> q_gen_825
<a, b, a>() -> q_gen_825
<b, a, b>() -> q_gen_825
<b, b, b>() -> q_gen_825
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_780, q_gen_781, q_gen_782},
Q_f={q_gen_780},
Delta=
{
<cons>(q_gen_782, q_gen_780) -> q_gen_780
<cons>(q_gen_782, q_gen_781) -> q_gen_780
<nil>() -> q_gen_781
<a>() -> q_gen_782
<b>() -> q_gen_782
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> not_null([cons(x, ll)]) -> 21  ;  (append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]) -> 49  ;  (append([cons(i, l1), l2, _r])) -> not_null([_r]) -> 22  ;  (not_null([nil])) -> BOT -> 22
}
Sat witness: Yes: ((append([t1, l2, _m])) -> append([cons(h1, t1), l2, cons(h1, _m)]), {
_m -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

Total time: 30.001800
Reason for stopping: DontKnow. Stopped because: timeout