Solving ../../benchmarks/true/append_not_null4.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, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)])}
(append([_kq, _lq, _mq]) /\ append([_kq, _lq, _nq])) -> eq_eltlist([_mq, _nq])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

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


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

Clause system for inference is:

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


Solving took 30.001166 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_1000, q_gen_1001, q_gen_1002, q_gen_1003, q_gen_1004, q_gen_1005, q_gen_1006, q_gen_1007, q_gen_1008, q_gen_1009, q_gen_1010, q_gen_1011, q_gen_1012, q_gen_1013, q_gen_1014, q_gen_1015, q_gen_1016, q_gen_1017, q_gen_1018, q_gen_1019, q_gen_1020, q_gen_904, q_gen_905, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_912, q_gen_913, q_gen_914, q_gen_915, q_gen_916, q_gen_917, q_gen_918, q_gen_919, q_gen_920, q_gen_921, q_gen_922, q_gen_924, q_gen_925, q_gen_926, q_gen_927, q_gen_928, q_gen_929, q_gen_930, q_gen_931, q_gen_932, q_gen_933, q_gen_934, q_gen_935, q_gen_936, q_gen_937, q_gen_938, q_gen_939, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946, q_gen_947, q_gen_948, q_gen_949, q_gen_950, q_gen_951, q_gen_952, q_gen_953, q_gen_954, q_gen_955, q_gen_956, q_gen_957, q_gen_958, q_gen_959, q_gen_960, q_gen_961, q_gen_962, q_gen_963, q_gen_964, q_gen_965, q_gen_966, q_gen_967, q_gen_968, q_gen_969, q_gen_970, q_gen_971, q_gen_972, q_gen_973, q_gen_974, q_gen_975, q_gen_976, q_gen_977, q_gen_978, q_gen_979, q_gen_980, q_gen_981, q_gen_982, q_gen_983, q_gen_984, q_gen_985, q_gen_986, q_gen_987, q_gen_988, q_gen_989, q_gen_990, q_gen_991, q_gen_992, q_gen_993, q_gen_994, q_gen_995, q_gen_996, q_gen_997, q_gen_998, q_gen_999},
Q_f={},
Delta=
{
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_927
<cons>(q_gen_927, q_gen_920) -> q_gen_935
<cons>(q_gen_921, q_gen_920) -> q_gen_975
<nil, nil>() -> q_gen_906
<nil, b>() -> q_gen_907
<b, nil>() -> q_gen_908
<b, b>() -> q_gen_909
<nil, a>() -> q_gen_913
<a, nil>() -> q_gen_914
<a, a>() -> q_gen_915
<cons, cons>(q_gen_915, q_gen_914, q_gen_913, q_gen_906) -> q_gen_918
<cons, b>(q_gen_921, q_gen_920) -> q_gen_919
<b, cons>(q_gen_921, q_gen_920) -> q_gen_922
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_925
<cons, b>(q_gen_927, q_gen_920) -> q_gen_926
<b, cons>(q_gen_927, q_gen_920) -> q_gen_928
<cons, a>(q_gen_927, q_gen_920) -> q_gen_930
<a, cons>(q_gen_927, q_gen_920) -> q_gen_931
<cons, cons>(q_gen_909, q_gen_928, q_gen_926, q_gen_925) -> q_gen_933
<cons, b>(q_gen_927, q_gen_935) -> q_gen_934
<b, cons>(q_gen_927, q_gen_935) -> q_gen_936
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_949
<a, cons>(q_gen_921, q_gen_920) -> q_gen_971
<a, b>() -> q_gen_972
<nil, cons>(q_gen_927, q_gen_920) -> q_gen_982
<b, a>() -> q_gen_983
<a, b, cons>(q_gen_927, q_gen_935) -> q_gen_1000
<cons, cons, cons>(q_gen_955, q_gen_1003, q_gen_944, q_gen_943, q_gen_952, q_gen_1002, q_gen_940, q_gen_939) -> q_gen_1001
<nil, a, cons>(q_gen_927, q_gen_920) -> q_gen_1002
<b, a, cons>(q_gen_927, q_gen_920) -> q_gen_1003
<cons, cons, cons>(q_gen_955, q_gen_1007, q_gen_944, q_gen_994, q_gen_1006, q_gen_1005, q_gen_991, q_gen_990) -> q_gen_1004
<cons, a, cons>(q_gen_909, q_gen_928, q_gen_907, q_gen_982) -> q_gen_1005
<cons, a, b>(q_gen_927, q_gen_920) -> q_gen_1006
<b, a, cons>(q_gen_927, q_gen_935) -> q_gen_1007
<cons, cons, cons>(q_gen_962, q_gen_1000, q_gen_1013, q_gen_1012, q_gen_958, q_gen_1011, q_gen_1010, q_gen_1009) -> q_gen_1008
<nil, cons, cons>(q_gen_909, q_gen_928, q_gen_907, q_gen_982) -> q_gen_1009
<nil, cons, a>(q_gen_927, q_gen_920) -> q_gen_1010
<nil, b, cons>(q_gen_927, q_gen_935) -> q_gen_1011
<a, cons, cons>(q_gen_909, q_gen_928, q_gen_907, q_gen_982) -> q_gen_1012
<a, cons, a>(q_gen_927, q_gen_920) -> q_gen_1013
<cons, cons, cons>(q_gen_967, q_gen_1016, q_gen_960, q_gen_999, q_gen_1015, q_gen_1005, q_gen_997, q_gen_990) -> q_gen_1014
<cons, a, a>(q_gen_927, q_gen_920) -> q_gen_1015
<a, a, cons>(q_gen_927, q_gen_935) -> q_gen_1016
<cons, cons, cons>(q_gen_955, q_gen_1003, q_gen_987, q_gen_1018, q_gen_952, q_gen_1002, q_gen_984, q_gen_937) -> q_gen_1017
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1018
<cons, cons, cons>(q_gen_967, q_gen_1016, q_gen_1013, q_gen_1012, q_gen_1015, q_gen_1005, q_gen_1020, q_gen_938) -> q_gen_1019
<cons, cons, a>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1020
<nil, nil, nil>() -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_905
<nil, cons, cons>(q_gen_915, q_gen_914, q_gen_913, q_gen_906) -> q_gen_912
<cons, nil, cons>(q_gen_915, q_gen_914, q_gen_913, q_gen_906) -> q_gen_916
<cons, nil, cons>(q_gen_909, q_gen_922, q_gen_919, q_gen_918) -> q_gen_917
<nil, cons, cons>(q_gen_909, q_gen_928, q_gen_926, q_gen_925) -> q_gen_924
<cons, nil, cons>(q_gen_915, q_gen_931, q_gen_930, q_gen_925) -> q_gen_929
<nil, cons, cons>(q_gen_909, q_gen_936, q_gen_934, q_gen_933) -> q_gen_932
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_937
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_939) -> q_gen_938
<nil, nil, cons>(q_gen_927, q_gen_920) -> q_gen_939
<nil, nil, b>() -> q_gen_940
<nil, b, cons>(q_gen_927, q_gen_920) -> q_gen_941
<nil, b, b>() -> q_gen_942
<b, nil, cons>(q_gen_927, q_gen_920) -> q_gen_943
<b, nil, b>() -> q_gen_944
<b, b, cons>(q_gen_927, q_gen_920) -> q_gen_945
<b, b, b>() -> q_gen_946
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_947
<cons, nil, cons>(q_gen_909, q_gen_922, q_gen_907, q_gen_949) -> q_gen_948
<cons, cons, cons>(q_gen_955, q_gen_954, q_gen_944, q_gen_953, q_gen_952, q_gen_951, q_gen_940, q_gen_947) -> q_gen_950
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_951
<nil, a, b>() -> q_gen_952
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_953
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_954
<b, a, b>() -> q_gen_955
<cons, cons, cons>(q_gen_962, q_gen_961, q_gen_960, q_gen_959, q_gen_958, q_gen_941, q_gen_957, q_gen_939) -> q_gen_956
<nil, nil, a>() -> q_gen_957
<nil, b, a>() -> q_gen_958
<a, nil, cons>(q_gen_927, q_gen_920) -> q_gen_959
<a, nil, a>() -> q_gen_960
<a, b, cons>(q_gen_927, q_gen_920) -> q_gen_961
<a, b, a>() -> q_gen_962
<cons, cons, cons>(q_gen_967, q_gen_966, q_gen_960, q_gen_965, q_gen_964, q_gen_951, q_gen_957, q_gen_947) -> q_gen_963
<nil, a, a>() -> q_gen_964
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_965
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_966
<a, a, a>() -> q_gen_967
<nil, cons, cons>(q_gen_909, q_gen_922, q_gen_919, q_gen_918) -> q_gen_968
<cons, cons, cons>(q_gen_946, q_gen_978, q_gen_977, q_gen_976, q_gen_942, q_gen_974, q_gen_973, q_gen_970) -> q_gen_969
<nil, cons, cons>(q_gen_972, q_gen_971, q_gen_907, q_gen_949) -> q_gen_970
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_973
<nil, b, cons>(q_gen_927, q_gen_975) -> q_gen_974
<b, cons, cons>(q_gen_972, q_gen_971, q_gen_907, q_gen_949) -> q_gen_976
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_977
<b, b, cons>(q_gen_927, q_gen_975) -> q_gen_978
<nil, cons, cons>(q_gen_915, q_gen_931, q_gen_930, q_gen_925) -> q_gen_979
<cons, cons, cons>(q_gen_955, q_gen_988, q_gen_987, q_gen_986, q_gen_952, q_gen_985, q_gen_984, q_gen_981) -> q_gen_980
<nil, cons, cons>(q_gen_983, q_gen_928, q_gen_913, q_gen_982) -> q_gen_981
<nil, cons, b>(q_gen_927, q_gen_920) -> q_gen_984
<nil, a, cons>(q_gen_921, q_gen_935) -> q_gen_985
<b, cons, cons>(q_gen_983, q_gen_928, q_gen_913, q_gen_982) -> q_gen_986
<b, cons, b>(q_gen_927, q_gen_920) -> q_gen_987
<b, a, cons>(q_gen_921, q_gen_935) -> q_gen_988
<cons, cons, cons>(q_gen_946, q_gen_995, q_gen_944, q_gen_994, q_gen_993, q_gen_992, q_gen_991, q_gen_990) -> q_gen_989
<cons, nil, cons>(q_gen_909, q_gen_928, q_gen_907, q_gen_982) -> q_gen_990
<cons, nil, b>(q_gen_927, q_gen_920) -> q_gen_991
<cons, b, cons>(q_gen_909, q_gen_928, q_gen_907, q_gen_982) -> q_gen_992
<cons, b, b>(q_gen_927, q_gen_920) -> q_gen_993
<b, nil, cons>(q_gen_927, q_gen_935) -> q_gen_994
<b, b, cons>(q_gen_927, q_gen_935) -> q_gen_995
<cons, cons, cons>(q_gen_962, q_gen_1000, q_gen_960, q_gen_999, q_gen_998, q_gen_992, q_gen_997, q_gen_990) -> q_gen_996
<cons, nil, a>(q_gen_927, q_gen_920) -> q_gen_997
<cons, b, a>(q_gen_927, q_gen_920) -> q_gen_998
<a, nil, cons>(q_gen_927, q_gen_935) -> q_gen_999
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_901, q_gen_902, q_gen_903, q_gen_910, q_gen_911, q_gen_923},
Q_f={},
Delta=
{
<cons>(q_gen_903, q_gen_902) -> q_gen_901
<nil>() -> q_gen_902
<b>() -> q_gen_903
<cons>(q_gen_911, q_gen_902) -> q_gen_910
<a>() -> q_gen_911
<cons>(q_gen_903, q_gen_901) -> q_gen_923
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004302 s (model generation: 0.003927,  model checking: 0.000375):

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

-------------------------------------------
Step 1, which took 0.003929 s (model generation: 0.003653,  model checking: 0.000276):

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

}

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

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([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 1  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 1  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 1  ;  (not_null([nil])) -> BOT -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.003552 s (model generation: 0.003544,  model checking: 0.000008):

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

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

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([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 1  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 1  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 1  ;  (not_null([nil])) -> BOT -> 4
}
Sat witness: Yes: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.003865 s (model generation: 0.003429,  model checking: 0.000436):

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

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

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

-------------------------------------------
Step 4, which took 0.003884 s (model generation: 0.003627,  model checking: 0.000257):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909},
Q_f={q_gen_904},
Delta=
{
<nil, nil>() -> q_gen_906
<nil, b>() -> q_gen_907
<b, nil>() -> q_gen_908
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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

-------------------------------------------
Step 5, which took 0.006940 s (model generation: 0.004848,  model checking: 0.002092):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909},
Q_f={q_gen_904},
Delta=
{
<nil, nil>() -> q_gen_906
<nil, b>() -> q_gen_907
<b, nil>() -> q_gen_908
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 3  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 3  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 4  ;  (not_null([nil])) -> BOT -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 6, which took 0.010583 s (model generation: 0.005285,  model checking: 0.005298):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909},
Q_f={q_gen_904},
Delta=
{
<nil, nil>() -> q_gen_906
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, nil>() -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 4  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 4  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 7  ;  (not_null([nil])) -> BOT -> 5
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 7, which took 0.007332 s (model generation: 0.006891,  model checking: 0.000441):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921},
Q_f={q_gen_904},
Delta=
{
<nil>() -> q_gen_920
<a>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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)]) -> 9  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 5  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 5  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 7  ;  (not_null([nil])) -> BOT -> 6
}
Sat witness: Yes: (() -> not_null([cons(x, ll)]), {
ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 8, which took 0.026518 s (model generation: 0.009573,  model checking: 0.016945):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921},
Q_f={q_gen_904},
Delta=
{
<nil>() -> q_gen_920
<a>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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)]) -> 9  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 6  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 6  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 7  ;  (not_null([nil])) -> BOT -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.010233 s (model generation: 0.004914,  model checking: 0.005319):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921},
Q_f={q_gen_904},
Delta=
{
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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)]) -> 9  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 7  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 7  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 10  ;  (not_null([nil])) -> BOT -> 8
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.013079 s (model generation: 0.005269,  model checking: 0.007810):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921},
Q_f={q_gen_904},
Delta=
{
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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)]) -> 10  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 8  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 8  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 10  ;  (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.009771 s (model generation: 0.005952,  model checking: 0.003819):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
}

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

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)]) -> 10  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 9  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 9  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 13  ;  (not_null([nil])) -> BOT -> 10
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.036024 s (model generation: 0.006960,  model checking: 0.029064):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, nil, b>() -> q_gen_940
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, b>() -> q_gen_942
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, nil, b>() -> q_gen_944
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, b>() -> q_gen_946
}

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

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

-------------------------------------------
Step 13, which took 0.074032 s (model generation: 0.008010,  model checking: 0.066022):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, nil, b>() -> q_gen_940
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, b>() -> q_gen_942
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, nil, b>() -> q_gen_944
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, b>() -> q_gen_946
}

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

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)]) -> 12  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 11  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 11  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 19  ;  (not_null([nil])) -> BOT -> 12
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.203683 s (model generation: 0.008871,  model checking: 0.194812):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, nil, b>() -> q_gen_940
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, a, b>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, nil, b>() -> q_gen_944
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 13  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 12  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 12  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 22  ;  (not_null([nil])) -> BOT -> 13
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.065004 s (model generation: 0.009748,  model checking: 0.055256):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, a, b>() -> q_gen_942
<nil, b, a>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 14  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 13  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 13  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 25  ;  (not_null([nil])) -> BOT -> 14
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 1.141625 s (model generation: 0.010541,  model checking: 1.131084):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, a, a>() -> q_gen_942
<nil, a, b>() -> q_gen_942
<nil, b, a>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 15  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 14  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 14  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 28  ;  (not_null([nil])) -> BOT -> 15
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.568430 s (model generation: 0.013900,  model checking: 0.554530):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, a, a>() -> q_gen_942
<nil, a, b>() -> q_gen_942
<nil, b, a>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 16  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 15  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 15  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 31  ;  (not_null([nil])) -> BOT -> 16
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(a, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 1.946666 s (model generation: 0.016904,  model checking: 1.929762):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, a, a>() -> q_gen_942
<nil, a, b>() -> q_gen_942
<nil, b, a>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 17  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 16  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 16  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 34  ;  (not_null([nil])) -> BOT -> 17
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 19, which took 0.722108 s (model generation: 0.020316,  model checking: 0.701792):

Model:
|_
{
append -> 
{{{
Q={q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_945, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, a>() -> q_gen_909
<b, b>() -> q_gen_909
<cons, cons, cons>(q_gen_946, q_gen_945, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<cons, nil, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<cons, b, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_941
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<cons, b, b>(q_gen_921, q_gen_920) -> q_gen_942
<nil, a, a>() -> q_gen_942
<nil, a, b>() -> q_gen_942
<nil, b, a>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_945
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_945
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 18  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 17  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 17  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 37  ;  (not_null([nil])) -> BOT -> 18
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 20, which took 1.659328 s (model generation: 0.022509,  model checking: 1.636819):

Model:
|_
{
append -> 
{{{
Q={q_gen_1000, q_gen_904, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_941, q_gen_942, q_gen_943, q_gen_944, q_gen_946},
Q_f={q_gen_904},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, a>() -> q_gen_909
<b, b>() -> q_gen_909
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<cons, cons, cons>(q_gen_946, q_gen_1000, q_gen_944, q_gen_943, q_gen_942, q_gen_941, q_gen_940, q_gen_904) -> q_gen_904
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_904
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_904
<nil, nil, nil>() -> q_gen_904
<cons, nil, a>(q_gen_921, q_gen_920) -> q_gen_940
<cons, nil, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<cons, b, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_941
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_941
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_941
<cons, b, a>(q_gen_921, q_gen_920) -> q_gen_942
<cons, b, b>(q_gen_921, q_gen_920) -> q_gen_942
<nil, a, a>() -> q_gen_942
<nil, a, b>() -> q_gen_942
<nil, b, a>() -> q_gen_942
<nil, b, b>() -> q_gen_942
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 19  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 18  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 18  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 40  ;  (not_null([nil])) -> BOT -> 19
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 21, which took 1.402953 s (model generation: 0.032483,  model checking: 1.370470):

Model:
|_
{
append -> 
{{{
Q={q_gen_1000, q_gen_1001, q_gen_1002, q_gen_1006, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_940, q_gen_943, q_gen_944, q_gen_946},
Q_f={q_gen_1001},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, a>() -> q_gen_909
<b, b>() -> q_gen_909
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<cons, cons, cons>(q_gen_946, q_gen_1000, q_gen_944, q_gen_943, q_gen_1006, q_gen_1002, q_gen_940, q_gen_1001) -> q_gen_1001
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1001
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1001
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1001
<nil, nil, nil>() -> q_gen_1001
<cons, a, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1002
<cons, b, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1002
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_1002
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_1002
<cons, a, b>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, b, a>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, b, b>(q_gen_921, q_gen_920) -> q_gen_1006
<nil, a, a>() -> q_gen_1006
<nil, a, b>() -> q_gen_1006
<nil, b, a>() -> q_gen_1006
<nil, b, b>() -> q_gen_1006
<cons, nil, a>(q_gen_921, q_gen_920) -> q_gen_940
<cons, nil, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_940
<nil, nil, a>() -> q_gen_940
<nil, nil, b>() -> q_gen_940
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_943
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_943
<a, nil, a>() -> q_gen_944
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_944
<b, nil, b>() -> q_gen_944
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 20  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 19  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 19  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 43  ;  (not_null([nil])) -> BOT -> 20
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 4.050889 s (model generation: 0.046312,  model checking: 4.004577):

Model:
|_
{
append -> 
{{{
Q={q_gen_1000, q_gen_1001, q_gen_1002, q_gen_1006, q_gen_1010, q_gen_1012, q_gen_1013, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_946},
Q_f={q_gen_1001},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, a>() -> q_gen_909
<b, b>() -> q_gen_909
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<cons, cons, cons>(q_gen_946, q_gen_1000, q_gen_1013, q_gen_1012, q_gen_1006, q_gen_1002, q_gen_1010, q_gen_1001) -> q_gen_1001
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1001
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1001
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1001
<nil, nil, nil>() -> q_gen_1001
<cons, a, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1002
<cons, b, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1002
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_1002
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_1002
<cons, a, b>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, b, a>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, b, b>(q_gen_921, q_gen_920) -> q_gen_1006
<nil, a, a>() -> q_gen_1006
<nil, a, b>() -> q_gen_1006
<nil, b, a>() -> q_gen_1006
<nil, b, b>() -> q_gen_1006
<cons, nil, a>(q_gen_921, q_gen_920) -> q_gen_1010
<cons, nil, b>(q_gen_921, q_gen_920) -> q_gen_1010
<nil, cons, a>(q_gen_921, q_gen_920) -> q_gen_1010
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_1010
<nil, nil, a>() -> q_gen_1010
<nil, nil, b>() -> q_gen_1010
<a, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1012
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1012
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1012
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1012
<a, cons, a>(q_gen_921, q_gen_920) -> q_gen_1013
<a, nil, a>() -> q_gen_1013
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_1013
<b, nil, b>() -> q_gen_1013
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 21  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 20  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 20  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 46  ;  (not_null([nil])) -> BOT -> 21
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 23, which took 1.891671 s (model generation: 0.048508,  model checking: 1.843163):

Model:
|_
{
append -> 
{{{
Q={q_gen_1000, q_gen_1001, q_gen_1002, q_gen_1006, q_gen_1010, q_gen_1012, q_gen_1013, q_gen_906, q_gen_907, q_gen_908, q_gen_909, q_gen_920, q_gen_921, q_gen_946},
Q_f={q_gen_1001},
Delta=
{
<cons>(q_gen_921, q_gen_920) -> q_gen_920
<nil>() -> q_gen_920
<a>() -> q_gen_921
<b>() -> q_gen_921
<cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_906
<nil, cons>(q_gen_921, q_gen_920) -> q_gen_906
<nil, nil>() -> q_gen_906
<cons, a>(q_gen_921, q_gen_920) -> q_gen_907
<cons, b>(q_gen_921, q_gen_920) -> q_gen_907
<nil, a>() -> q_gen_907
<nil, b>() -> q_gen_907
<a, cons>(q_gen_921, q_gen_920) -> q_gen_908
<a, nil>() -> q_gen_908
<b, cons>(q_gen_921, q_gen_920) -> q_gen_908
<b, nil>() -> q_gen_908
<a, a>() -> q_gen_909
<a, b>() -> q_gen_909
<b, a>() -> q_gen_909
<b, b>() -> q_gen_909
<a, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<a, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, a, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<b, b, cons>(q_gen_921, q_gen_920) -> q_gen_1000
<cons, cons, cons>(q_gen_946, q_gen_1000, q_gen_1013, q_gen_1012, q_gen_1006, q_gen_1002, q_gen_1010, q_gen_1001) -> q_gen_1001
<cons, nil, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1001
<nil, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1001
<nil, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1001
<nil, nil, nil>() -> q_gen_1001
<cons, a, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1002
<cons, b, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1002
<nil, a, cons>(q_gen_921, q_gen_920) -> q_gen_1002
<nil, b, cons>(q_gen_921, q_gen_920) -> q_gen_1002
<cons, a, a>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, a, b>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, b, a>(q_gen_921, q_gen_920) -> q_gen_1006
<cons, b, b>(q_gen_921, q_gen_920) -> q_gen_1006
<nil, a, a>() -> q_gen_1006
<nil, a, b>() -> q_gen_1006
<nil, b, a>() -> q_gen_1006
<nil, b, b>() -> q_gen_1006
<cons, nil, a>(q_gen_921, q_gen_920) -> q_gen_1010
<cons, nil, b>(q_gen_921, q_gen_920) -> q_gen_1010
<nil, cons, a>(q_gen_921, q_gen_920) -> q_gen_1010
<nil, cons, b>(q_gen_921, q_gen_920) -> q_gen_1010
<nil, nil, a>() -> q_gen_1010
<nil, nil, b>() -> q_gen_1010
<a, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1012
<a, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1012
<b, cons, cons>(q_gen_909, q_gen_908, q_gen_907, q_gen_906) -> q_gen_1012
<b, nil, cons>(q_gen_921, q_gen_920) -> q_gen_1012
<a, cons, a>(q_gen_921, q_gen_920) -> q_gen_1013
<a, nil, a>() -> q_gen_1013
<b, cons, b>(q_gen_921, q_gen_920) -> q_gen_1013
<b, nil, b>() -> q_gen_1013
<a, a, a>() -> q_gen_946
<a, b, a>() -> q_gen_946
<b, a, b>() -> q_gen_946
<b, b, b>() -> q_gen_946
}

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

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)]) -> 22  ;  (append([l1, l2, _oq]) /\ not_null([l1])) -> not_null([_oq]) -> 21  ;  (append([l1, l2, _pq]) /\ not_null([l2])) -> not_null([_pq]) -> 21  ;  (append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]) -> 49  ;  (not_null([nil])) -> BOT -> 22
}
Sat witness: Yes: ((append([t1, l2, _jq])) -> append([cons(h1, t1), l2, cons(h1, _jq)]), {
_jq -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(b, nil)
})

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