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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)])}
(append([_uy, _vy, _wy]) /\ append([_uy, _vy, _xy])) -> eq_eltlist([_wy, _xy])
)
(length, F:
{() -> length([nil, z])
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)])}
(length([_zy, _az]) /\ length([_zy, _bz])) -> eq_nat([_az, _bz])
)
}

properties:
{(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 0
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 0
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 0
}


Solving took 65.766827 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4845, q_gen_4846, q_gen_4847, q_gen_4850, q_gen_4851, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4856, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4863, q_gen_4864, q_gen_4865, q_gen_4866, q_gen_4867, q_gen_4868, q_gen_4870, q_gen_4871, q_gen_4872, q_gen_4873, q_gen_4874, q_gen_4875, q_gen_4876, q_gen_4877, q_gen_4878, q_gen_4879, q_gen_4880, q_gen_4881, q_gen_4882, q_gen_4883, q_gen_4884, q_gen_4885, q_gen_4886, q_gen_4887, q_gen_4888, q_gen_4889, q_gen_4890, q_gen_4891, q_gen_4892, q_gen_4893, q_gen_4894, q_gen_4895, q_gen_4896, q_gen_4897, q_gen_4898, q_gen_4900, q_gen_4901, q_gen_4902, q_gen_4903, q_gen_4904, q_gen_4905, q_gen_4906, q_gen_4908, q_gen_4909, q_gen_4910, q_gen_4911, q_gen_4912, q_gen_4913, q_gen_4914, q_gen_4915, q_gen_4916, q_gen_4917, q_gen_4919, q_gen_4920, q_gen_4921, q_gen_4922, q_gen_4923, q_gen_4925, q_gen_4926, q_gen_4927, q_gen_4928, q_gen_4929, q_gen_4930, q_gen_4931, q_gen_4934, q_gen_4935, q_gen_4936, q_gen_4937, q_gen_4938, q_gen_4939, q_gen_4941, q_gen_4942, q_gen_4943, q_gen_4944, q_gen_4945, q_gen_4946, q_gen_4947, q_gen_4948, q_gen_4949, q_gen_4950, q_gen_4951, q_gen_4952, q_gen_4953, q_gen_4954, q_gen_4955, q_gen_4956, q_gen_4957, q_gen_4958, q_gen_4959, q_gen_4960, q_gen_4961, q_gen_4965, q_gen_4966, q_gen_4967, q_gen_4968, q_gen_4969, q_gen_4970, q_gen_4971, q_gen_4973, q_gen_4974, q_gen_4975, q_gen_4977, q_gen_4978, q_gen_4979, q_gen_4980, q_gen_4981, q_gen_4982, q_gen_4983, q_gen_4984, q_gen_4985, q_gen_4986, q_gen_4987, q_gen_4988, q_gen_4989, q_gen_4990, q_gen_4991, q_gen_4992, q_gen_4993, q_gen_4994, q_gen_4995, q_gen_4996, q_gen_4997},
Q_f={},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<a>() -> q_gen_4883
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4896
<nil, nil>() -> q_gen_4843
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4846
<a, a>() -> q_gen_4847
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4873
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4891
<b, a>() -> q_gen_4905
<nil, cons>(q_gen_4883, q_gen_4853) -> q_gen_4922
<a, b>() -> q_gen_4923
<nil, cons>(q_gen_4854, q_gen_4896) -> q_gen_4927
<cons, cons>(q_gen_4844, q_gen_4922) -> q_gen_4945
<nil, nil, nil>() -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<nil, cons, cons>(q_gen_4847, q_gen_4846) -> q_gen_4845
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4850
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4851
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4856
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<cons, cons, cons>(q_gen_4859, q_gen_4864) -> q_gen_4863
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4866
<cons, cons, cons>(q_gen_4855, q_gen_4868) -> q_gen_4867
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4868
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4870
<nil, cons, cons>(q_gen_4844, q_gen_4873) -> q_gen_4872
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4874
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4875
<cons, cons, cons>(q_gen_4855, q_gen_4877) -> q_gen_4876
<cons, cons, cons>(q_gen_4855, q_gen_4870) -> q_gen_4877
<cons, cons, cons>(q_gen_4855, q_gen_4851) -> q_gen_4878
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4879
<nil, cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4880
<cons, cons, cons>(q_gen_4884, q_gen_4882) -> q_gen_4881
<nil, nil, cons>(q_gen_4883, q_gen_4853) -> q_gen_4882
<b, a, b>() -> q_gen_4884
<cons, cons, cons>(q_gen_4886, q_gen_4882) -> q_gen_4885
<a, a, a>() -> q_gen_4886
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4887
<cons, cons, cons>(q_gen_4855, q_gen_4850) -> q_gen_4888
<cons, cons, cons>(q_gen_4859, q_gen_4890) -> q_gen_4889
<cons, nil, cons>(q_gen_4844, q_gen_4891) -> q_gen_4890
<cons, cons, cons>(q_gen_4855, q_gen_4875) -> q_gen_4892
<cons, cons, cons>(q_gen_4859, q_gen_4894) -> q_gen_4893
<cons, cons, cons>(q_gen_4855, q_gen_4895) -> q_gen_4894
<nil, nil, cons>(q_gen_4854, q_gen_4896) -> q_gen_4895
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4897
<cons, cons, cons>(q_gen_4884, q_gen_4839) -> q_gen_4898
<cons, cons, cons>(q_gen_4855, q_gen_4901) -> q_gen_4900
<nil, cons, cons>(q_gen_4847, q_gen_4891) -> q_gen_4901
<cons, cons, cons>(q_gen_4859, q_gen_4903) -> q_gen_4902
<cons, cons, cons>(q_gen_4884, q_gen_4904) -> q_gen_4903
<nil, cons, cons>(q_gen_4905, q_gen_4871) -> q_gen_4904
<cons, cons, cons>(q_gen_4884, q_gen_4852) -> q_gen_4906
<cons, cons, cons>(q_gen_4886, q_gen_4909) -> q_gen_4908
<cons, cons, cons>(q_gen_4886, q_gen_4860) -> q_gen_4909
<cons, cons, cons>(q_gen_4886, q_gen_4911) -> q_gen_4910
<cons, cons, cons>(q_gen_4886, q_gen_4912) -> q_gen_4911
<cons, cons, cons>(q_gen_4859, q_gen_4842) -> q_gen_4912
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4913
<cons, cons, cons>(q_gen_4855, q_gen_4915) -> q_gen_4914
<cons, cons, cons>(q_gen_4884, q_gen_4875) -> q_gen_4915
<cons, cons, cons>(q_gen_4859, q_gen_4917) -> q_gen_4916
<cons, cons, cons>(q_gen_4884, q_gen_4894) -> q_gen_4917
<nil, cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4919
<cons, cons, cons>(q_gen_4859, q_gen_4921) -> q_gen_4920
<nil, cons, cons>(q_gen_4923, q_gen_4922) -> q_gen_4921
<cons, cons, cons>(q_gen_4859, q_gen_4863) -> q_gen_4925
<cons, nil, cons>(q_gen_4844, q_gen_4927) -> q_gen_4926
<cons, cons, cons>(q_gen_4859, q_gen_4929) -> q_gen_4928
<cons, cons, cons>(q_gen_4884, q_gen_4864) -> q_gen_4929
<cons, cons, cons>(q_gen_4884, q_gen_4931) -> q_gen_4930
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4931
<cons, cons, cons>(q_gen_4859, q_gen_4935) -> q_gen_4934
<nil, cons, cons>(q_gen_4923, q_gen_4858) -> q_gen_4935
<cons, cons, cons>(q_gen_4855, q_gen_4937) -> q_gen_4936
<cons, cons, cons>(q_gen_4886, q_gen_4864) -> q_gen_4937
<cons, cons, cons>(q_gen_4886, q_gen_4863) -> q_gen_4938
<cons, cons, cons>(q_gen_4886, q_gen_4898) -> q_gen_4939
<cons, cons, cons>(q_gen_4859, q_gen_4942) -> q_gen_4941
<cons, nil, cons>(q_gen_4844, q_gen_4922) -> q_gen_4942
<cons, cons, cons>(q_gen_4859, q_gen_4944) -> q_gen_4943
<cons, nil, cons>(q_gen_4847, q_gen_4945) -> q_gen_4944
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4946
<cons, cons, cons>(q_gen_4884, q_gen_4868) -> q_gen_4947
<cons, cons, cons>(q_gen_4884, q_gen_4929) -> q_gen_4948
<cons, cons, cons>(q_gen_4884, q_gen_4950) -> q_gen_4949
<cons, cons, cons>(q_gen_4884, q_gen_4870) -> q_gen_4950
<cons, cons, cons>(q_gen_4884, q_gen_4952) -> q_gen_4951
<cons, cons, cons>(q_gen_4855, q_gen_4953) -> q_gen_4952
<nil, cons, cons>(q_gen_4844, q_gen_4891) -> q_gen_4953
<cons, cons, cons>(q_gen_4884, q_gen_4955) -> q_gen_4954
<cons, cons, cons>(q_gen_4855, q_gen_4892) -> q_gen_4955
<cons, cons, cons>(q_gen_4884, q_gen_4957) -> q_gen_4956
<cons, nil, cons>(q_gen_4847, q_gen_4922) -> q_gen_4957
<cons, cons, cons>(q_gen_4859, q_gen_4959) -> q_gen_4958
<cons, cons, cons>(q_gen_4886, q_gen_4931) -> q_gen_4959
<cons, cons, cons>(q_gen_4884, q_gen_4961) -> q_gen_4960
<cons, cons, cons>(q_gen_4886, q_gen_4929) -> q_gen_4961
<cons, cons, cons>(q_gen_4855, q_gen_4966) -> q_gen_4965
<cons, cons, cons>(q_gen_4859, q_gen_4866) -> q_gen_4966
<cons, cons, cons>(q_gen_4855, q_gen_4968) -> q_gen_4967
<cons, cons, cons>(q_gen_4855, q_gen_4969) -> q_gen_4968
<cons, cons, cons>(q_gen_4859, q_gen_4868) -> q_gen_4969
<cons, cons, cons>(q_gen_4886, q_gen_4926) -> q_gen_4970
<cons, cons, cons>(q_gen_4886, q_gen_4862) -> q_gen_4971
<cons, cons, cons>(q_gen_4855, q_gen_4863) -> q_gen_4973
<cons, cons, cons>(q_gen_4855, q_gen_4946) -> q_gen_4974
<cons, cons, cons>(q_gen_4855, q_gen_4947) -> q_gen_4975
<cons, cons, cons>(q_gen_4884, q_gen_4978) -> q_gen_4977
<cons, cons, cons>(q_gen_4859, q_gen_4979) -> q_gen_4978
<cons, cons, cons>(q_gen_4886, q_gen_4839) -> q_gen_4979
<cons, cons, cons>(q_gen_4886, q_gen_4981) -> q_gen_4980
<cons, cons, cons>(q_gen_4855, q_gen_4982) -> q_gen_4981
<cons, cons, cons>(q_gen_4886, q_gen_4983) -> q_gen_4982
<cons, nil, cons>(q_gen_4847, q_gen_4843) -> q_gen_4983
<cons, cons, cons>(q_gen_4884, q_gen_4862) -> q_gen_4984
<nil, cons, cons>(q_gen_4847, q_gen_4873) -> q_gen_4985
<cons, cons, cons>(q_gen_4884, q_gen_4987) -> q_gen_4986
<nil, cons, cons>(q_gen_4905, q_gen_4858) -> q_gen_4987
<cons, cons, cons>(q_gen_4859, q_gen_4867) -> q_gen_4988
<cons, cons, cons>(q_gen_4884, q_gen_4879) -> q_gen_4989
<cons, cons, cons>(q_gen_4884, q_gen_4866) -> q_gen_4990
<cons, cons, cons>(q_gen_4884, q_gen_4867) -> q_gen_4991
<cons, cons, cons>(q_gen_4859, q_gen_4993) -> q_gen_4992
<cons, cons, cons>(q_gen_4884, q_gen_4994) -> q_gen_4993
<cons, cons, cons>(q_gen_4884, q_gen_4995) -> q_gen_4994
<cons, nil, cons>(q_gen_4905, q_gen_4843) -> q_gen_4995
<cons, cons, cons>(q_gen_4884, q_gen_4997) -> q_gen_4996
<cons, cons, cons>(q_gen_4859, q_gen_4874) -> q_gen_4997
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4840, q_gen_4841, q_gen_4848, q_gen_4849, q_gen_4861, q_gen_4869, q_gen_4899, q_gen_4907, q_gen_4918, q_gen_4924, q_gen_4932, q_gen_4933, q_gen_4940, q_gen_4962, q_gen_4963, q_gen_4964, q_gen_4972, q_gen_4976, q_gen_4998, q_gen_4999, q_gen_5000},
Q_f={},
Delta=
{
<b>() -> q_gen_4841
<a>() -> q_gen_4849
<nil, z>() -> q_gen_4838
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4840
<cons, s>(q_gen_4849, q_gen_4838) -> q_gen_4848
<cons, s>(q_gen_4841, q_gen_4840) -> q_gen_4861
<cons, s>(q_gen_4841, q_gen_4861) -> q_gen_4869
<cons, s>(q_gen_4849, q_gen_4840) -> q_gen_4899
<cons, s>(q_gen_4849, q_gen_4861) -> q_gen_4907
<cons, s>(q_gen_4841, q_gen_4869) -> q_gen_4918
<cons, s>(q_gen_4841, q_gen_4899) -> q_gen_4924
<cons, s>(q_gen_4849, q_gen_4869) -> q_gen_4932
<cons, s>(q_gen_4841, q_gen_4848) -> q_gen_4933
<cons, s>(q_gen_4849, q_gen_4907) -> q_gen_4940
<cons, s>(q_gen_4849, q_gen_4963) -> q_gen_4962
<cons, s>(q_gen_4849, q_gen_4848) -> q_gen_4963
<cons, s>(q_gen_4841, q_gen_4932) -> q_gen_4964
<cons, s>(q_gen_4849, q_gen_4918) -> q_gen_4972
<cons, s>(q_gen_4841, q_gen_4918) -> q_gen_4976
<cons, s>(q_gen_4849, q_gen_4999) -> q_gen_4998
<cons, s>(q_gen_4841, q_gen_4933) -> q_gen_4999
<cons, s>(q_gen_4841, q_gen_4940) -> q_gen_5000
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006357 s (model generation: 0.005902,  model checking: 0.000455):

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 3
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 1
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 1, which took 0.005552 s (model generation: 0.005132,  model checking: 0.000420):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838},
Q_f={q_gen_4838},
Delta=
{
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 1
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.006925 s (model generation: 0.006641,  model checking: 0.000284):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838},
Q_f={q_gen_4838},
Delta=
{
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 1
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 4
}
Sat witness: Found: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 3, which took 0.005744 s (model generation: 0.005523,  model checking: 0.000221):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 1
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 4
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.005517 s (model generation: 0.005001,  model checking: 0.000516):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844},
Q_f={q_gen_4839},
Delta=
{
<nil, nil>() -> q_gen_4843
<b, b>() -> q_gen_4844
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 2
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 4
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 5, which took 0.006201 s (model generation: 0.005698,  model checking: 0.000503):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844},
Q_f={q_gen_4839},
Delta=
{
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 3
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 4
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 7
}
Sat witness: Found: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 6, which took 0.006609 s (model generation: 0.005016,  model checking: 0.001593):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844},
Q_f={q_gen_4839},
Delta=
{
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 4
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 7
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.007128 s (model generation: 0.006758,  model checking: 0.000370):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 7
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 7
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 7
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> nil  ;  _dz -> z  ;  _ez -> cons(b, nil)  ;  _fz -> s(z)  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 8, which took 0.008196 s (model generation: 0.006526,  model checking: 0.001670):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 5
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 7
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 10
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 8
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 9, which took 0.007310 s (model generation: 0.006897,  model checking: 0.000413):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 6
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 10
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 10
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 8
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, nil)  ;  _fz -> s(z)  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.009506 s (model generation: 0.007570,  model checking: 0.001936):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 7
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 10
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 13
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 9
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.010408 s (model generation: 0.008936,  model checking: 0.001472):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> length([nil, z]) -> 8
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 13
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 13
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 10
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, nil)  ;  _dz -> s(z)  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 12, which took 0.009941 s (model generation: 0.008063,  model checking: 0.001878):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 9
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 13
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 16
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 11
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.011918 s (model generation: 0.010800,  model checking: 0.001118):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4847, q_gen_4850, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<b, b>() -> q_gen_4844
<a, a>() -> q_gen_4847
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4850
<cons, cons, cons>(q_gen_4855, q_gen_4850) -> q_gen_4850
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4850
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4850
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 10
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 13
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 16
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 11
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.011169 s (model generation: 0.008966,  model checking: 0.002203):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 11
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 16
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 16
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 12
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 15, which took 0.013151 s (model generation: 0.010676,  model checking: 0.002475):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 12
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 16
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 19
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.011559 s (model generation: 0.010913,  model checking: 0.000646):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 13
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 19
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 19
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 14
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> nil  ;  _dz -> z  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 17, which took 0.012087 s (model generation: 0.011278,  model checking: 0.000809):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4840, q_gen_4841, q_gen_4861},
Q_f={q_gen_4838, q_gen_4840},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<nil, z>() -> q_gen_4838
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4840
<cons, s>(q_gen_4841, q_gen_4861) -> q_gen_4840
<cons, s>(q_gen_4841, q_gen_4840) -> q_gen_4861
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 14
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 19
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 19
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 17
}
Sat witness: Found: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(z)  ;  ll -> cons(b, nil)  ;  x -> b
})

-------------------------------------------
Step 18, which took 0.012707 s (model generation: 0.010807,  model checking: 0.001900):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4862, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> length([nil, z]) -> 15
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 19
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 22
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 18
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.012827 s (model generation: 0.011667,  model checking: 0.001160):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> length([nil, z]) -> 16
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 22
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 22
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 19
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, nil)  ;  _dz -> s(z)  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 20, which took 0.015858 s (model generation: 0.014382,  model checking: 0.001476):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> length([nil, z]) -> 17
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 22
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 25
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 20
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 21, which took 0.016772 s (model generation: 0.015162,  model checking: 0.001610):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> length([nil, z]) -> 18
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 25
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 25
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 21
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 22, which took 0.020822 s (model generation: 0.016518,  model checking: 0.004304):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> length([nil, z]) -> 19
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 25
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 28
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 22
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.022160 s (model generation: 0.020915,  model checking: 0.001245):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4856, q_gen_4858, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839, q_gen_4856},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4856) -> q_gen_4856
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4856
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21
() -> length([nil, z]) -> 20
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 28
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 28
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 23
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, nil)  ;  _dz -> s(z)  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> nil  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.026847 s (model generation: 0.020838,  model checking: 0.006009):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4864, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 21
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 28
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 31
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 24
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 25, which took 0.023321 s (model generation: 0.021935,  model checking: 0.001386):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4845, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4845},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4845) -> q_gen_4845
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4845
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4845
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> length([nil, z]) -> 22
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 31
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 31
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 25
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 26, which took 0.029194 s (model generation: 0.023886,  model checking: 0.005308):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
() -> length([nil, z]) -> 23
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 31
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 34
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 26
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 27, which took 0.027397 s (model generation: 0.026240,  model checking: 0.001157):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4864, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
() -> length([nil, z]) -> 24
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 34
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 34
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 27
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, nil)  ;  _dz -> s(z)  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> nil  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 0.045700 s (model generation: 0.026030,  model checking: 0.019670):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> length([nil, z]) -> 25
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 34
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 37
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 28
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 29, which took 0.038213 s (model generation: 0.036274,  model checking: 0.001939):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4862, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, b, b>() -> q_gen_4855
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> length([nil, z]) -> 26
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 37
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 37
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 29
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, nil)  ;  _fz -> s(z)  ;  l1 -> cons(a, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 30, which took 0.062031 s (model generation: 0.042067,  model checking: 0.019964):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> length([nil, z]) -> 27
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 37
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 40
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 30
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(a, cons(b, cons(b, nil))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 31, which took 0.064353 s (model generation: 0.062736,  model checking: 0.001617):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4857
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4857
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
() -> length([nil, z]) -> 28
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 40
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 40
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 31
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(a, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 32, which took 0.074297 s (model generation: 0.069887,  model checking: 0.004410):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> length([nil, z]) -> 29
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 40
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 43
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 32
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(a, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, cons(b, nil)))  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 33, which took 0.102374 s (model generation: 0.100495,  model checking: 0.001879):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> length([nil, z]) -> 30
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 43
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 43
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 33
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 34, which took 0.129298 s (model generation: 0.124077,  model checking: 0.005221):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4864, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
() -> length([nil, z]) -> 31
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 43
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 46
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 34
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(b, nil)))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 35, which took 0.324780 s (model generation: 0.324119,  model checking: 0.000661):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4846, q_gen_4847, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4862, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<nil, nil>() -> q_gen_4843
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4846
<cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4846
<cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4846
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4846
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4846
<a, a>() -> q_gen_4847
<b, a>() -> q_gen_4847
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4847, q_gen_4846) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4846) -> q_gen_4852
<nil, cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4862
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
() -> length([nil, z]) -> 32
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 43
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 46
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 34
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 36, which took 0.393463 s (model generation: 0.391459,  model checking: 0.002004):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4851, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4851},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4851) -> q_gen_4851
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4851
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> length([nil, z]) -> 33
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 46
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 46
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 35
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _fz -> s(s(s(s(z))))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 37, which took 0.161039 s (model generation: 0.137068,  model checking: 0.023971):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4864, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 37
() -> length([nil, z]) -> 34
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 46
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 49
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 36
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 38, which took 0.120246 s (model generation: 0.118820,  model checking: 0.001426):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4864, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> length([nil, z]) -> 35
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 49
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 49
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 37
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _dz -> s(s(s(s(z))))  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(b, cons(b, nil))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 39, which took 0.129357 s (model generation: 0.129041,  model checking: 0.000316):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4851, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858},
Q_f={q_gen_4839, q_gen_4851},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4851) -> q_gen_4851
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4851
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4840, q_gen_4841, q_gen_4861, q_gen_4869},
Q_f={q_gen_4838, q_gen_4840, q_gen_4861},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<nil, z>() -> q_gen_4838
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4840
<cons, s>(q_gen_4841, q_gen_4840) -> q_gen_4861
<cons, s>(q_gen_4841, q_gen_4861) -> q_gen_4869
<cons, s>(q_gen_4841, q_gen_4869) -> q_gen_4869
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> length([nil, z]) -> 36
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 49
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 49
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 40
}
Sat witness: Found: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(s(z))  ;  ll -> cons(a, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 40, which took 0.131563 s (model generation: 0.130480,  model checking: 0.001083):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4862, q_gen_4863, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<cons, cons, cons>(q_gen_4855, q_gen_4863) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<cons, cons, cons>(q_gen_4859, q_gen_4863) -> q_gen_4863
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4863
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> length([nil, z]) -> 37
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 49
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 52
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 41
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 41, which took 0.139172 s (model generation: 0.137578,  model checking: 0.001594):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865, q_gen_4871, q_gen_4891},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4891
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4891) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4891) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
() -> length([nil, z]) -> 38
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 52
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 52
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 42
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _dz -> s(s(s(s(z))))  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 42, which took 0.155630 s (model generation: 0.138445,  model checking: 0.017185):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865, q_gen_4871, q_gen_4896},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4896
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4896) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
() -> length([nil, z]) -> 39
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 52
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 55
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 43
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 43, which took 0.150682 s (model generation: 0.149802,  model checking: 0.000880):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4865, q_gen_4871, q_gen_4896},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4896
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, cons>(q_gen_4854, q_gen_4896) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, cons>(q_gen_4854, q_gen_4896) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
() -> length([nil, z]) -> 40
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 55
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 55
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 44
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> nil  ;  _dz -> z  ;  _ez -> cons(b, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> nil  ;  l2 -> nil
})

-------------------------------------------
Step 44, which took 0.191384 s (model generation: 0.188893,  model checking: 0.002491):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4862, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4859, q_gen_4864) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4864
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4864
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 43
() -> length([nil, z]) -> 41
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 55
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 58
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 45
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 45, which took 0.192874 s (model generation: 0.190891,  model checking: 0.001983):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4862, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4859, q_gen_4864) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4864
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 44
() -> length([nil, z]) -> 42
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 58
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 58
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 46
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  _dz -> s(s(s(s(z))))  ;  _ez -> cons(b, cons(a, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 46, which took 0.269154 s (model generation: 0.261893,  model checking: 0.007261):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 45
() -> length([nil, z]) -> 43
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 58
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 61
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 47
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 47, which took 0.245461 s (model generation: 0.240362,  model checking: 0.005099):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 46
() -> length([nil, z]) -> 44
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 61
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 61
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 48
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(a, cons(a, cons(b, cons(b, nil))))  ;  _fz -> s(s(s(s(z))))  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 48, which took 0.359112 s (model generation: 0.356631,  model checking: 0.002481):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 47
() -> length([nil, z]) -> 45
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 61
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 64
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 49
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, cons(a, nil)))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 49, which took 0.424820 s (model generation: 0.421494,  model checking: 0.003326):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4857
<cons, cons, cons>(q_gen_4859, q_gen_4864) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 48
() -> length([nil, z]) -> 46
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 64
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 64
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 50
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _fz -> s(s(s(s(z))))  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 50, which took 0.460581 s (model generation: 0.455837,  model checking: 0.004744):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 49
() -> length([nil, z]) -> 47
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 64
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 67
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 51
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 51, which took 1.387518 s (model generation: 1.386011,  model checking: 0.001507):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 50
() -> length([nil, z]) -> 48
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 67
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 67
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 52
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, nil)  ;  _dz -> s(z)  ;  _ez -> cons(b, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(a, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 52, which took 1.387692 s (model generation: 1.382080,  model checking: 0.005612):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 51
() -> length([nil, z]) -> 49
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 67
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 70
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 53
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 53, which took 1.221074 s (model generation: 1.218364,  model checking: 0.002710):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 52
() -> length([nil, z]) -> 50
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 70
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 70
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 54
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, nil))  ;  _dz -> s(s(z))  ;  _ez -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  _fz -> s(s(s(s(z))))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 54, which took 0.654502 s (model generation: 0.651693,  model checking: 0.002809):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 53
() -> length([nil, z]) -> 51
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 70
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 73
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 55
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 55, which took 0.671358 s (model generation: 0.668146,  model checking: 0.003212):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 54
() -> length([nil, z]) -> 52
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 73
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 73
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 56
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(a, cons(a, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(b, cons(a, cons(b, cons(b, cons(b, nil)))))  ;  _fz -> s(s(s(s(s(z)))))  ;  l1 -> cons(a, cons(a, cons(a, nil)))  ;  l2 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 56, which took 0.749618 s (model generation: 0.744658,  model checking: 0.004960):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 55
() -> length([nil, z]) -> 53
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 73
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 76
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 57
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(a, cons(b, cons(b, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  t1 -> cons(b, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 57, which took 2.142078 s (model generation: 2.138493,  model checking: 0.003585):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4862
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 56
() -> length([nil, z]) -> 54
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 76
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 76
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 58
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  _dz -> s(s(s(s(s(z)))))  ;  _ez -> cons(a, cons(b, cons(b, nil)))  ;  _fz -> s(s(s(z)))  ;  l1 -> cons(a, cons(b, nil))  ;  l2 -> cons(a, nil)
})

-------------------------------------------
Step 58, which took 2.528020 s (model generation: 2.524862,  model checking: 0.003158):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4862
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 57
() -> length([nil, z]) -> 55
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 76
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 79
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 59
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 59, which took 2.038386 s (model generation: 2.034626,  model checking: 0.003760):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4860, q_gen_4863, q_gen_4865, q_gen_4871, q_gen_4884},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4863) -> q_gen_4839
<cons, cons, cons>(q_gen_4884, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4884, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4884, q_gen_4863) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4884, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4863
<b, a, b>() -> q_gen_4884
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 58
() -> length([nil, z]) -> 56
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 79
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 79
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 60
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(a, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(b, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  _fz -> s(s(s(s(s(z)))))  ;  l1 -> cons(b, cons(a, cons(b, nil)))  ;  l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 60, which took 2.924644 s (model generation: 2.924275,  model checking: 0.000369):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4846, q_gen_4847, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4859, q_gen_4864, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4846
<cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4846
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4846
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4846
<a, a>() -> q_gen_4847
<a, b>() -> q_gen_4847
<b, a>() -> q_gen_4847
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4847, q_gen_4846) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4864) -> q_gen_4852
<cons, nil, cons>(q_gen_4847, q_gen_4846) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4857
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4846) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4864) -> q_gen_4864
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4864
<nil, cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4864
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4864
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 61
() -> length([nil, z]) -> 57
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 79
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 79
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 60
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 61, which took 5.531970 s (model generation: 5.527305,  model checking: 0.004665):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4842
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 62
() -> length([nil, z]) -> 58
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 79
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 82
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 61
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(a, cons(a, nil)))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, cons(a, nil)))  ;  t1 -> cons(b, cons(a, cons(a, nil)))
})

-------------------------------------------
Step 62, which took 3.781204 s (model generation: 3.777967,  model checking: 0.003237):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, cons, cons>(q_gen_4859, q_gen_4842) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 63
() -> length([nil, z]) -> 59
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 82
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 82
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 62
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(a, cons(b, nil))  ;  _fz -> s(s(z))  ;  l1 -> cons(b, nil)  ;  l2 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 63, which took 6.843938 s (model generation: 6.839427,  model checking: 0.004511):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4865, q_gen_4886},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4839
<cons, cons, cons>(q_gen_4886, q_gen_4839) -> q_gen_4839
<cons, cons, cons>(q_gen_4886, q_gen_4852) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4886, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4862
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4862
<cons, cons, cons>(q_gen_4886, q_gen_4862) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<a, a, a>() -> q_gen_4886
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 64
() -> length([nil, z]) -> 60
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 82
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 85
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 63
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(a, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 64, which took 5.988860 s (model generation: 5.986770,  model checking: 0.002090):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858},
Q_f={q_gen_4839, q_gen_4842},
Delta=
{
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4853
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<a, b, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4840, q_gen_4841, q_gen_4849, q_gen_4861, q_gen_4869},
Q_f={q_gen_4838, q_gen_4840, q_gen_4861},
Delta=
{
<b>() -> q_gen_4841
<a>() -> q_gen_4849
<cons, s>(q_gen_4849, q_gen_4838) -> q_gen_4838
<cons, s>(q_gen_4849, q_gen_4840) -> q_gen_4838
<nil, z>() -> q_gen_4838
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4840
<cons, s>(q_gen_4841, q_gen_4840) -> q_gen_4861
<cons, s>(q_gen_4841, q_gen_4861) -> q_gen_4869
<cons, s>(q_gen_4841, q_gen_4869) -> q_gen_4869
<cons, s>(q_gen_4849, q_gen_4861) -> q_gen_4869
<cons, s>(q_gen_4849, q_gen_4869) -> q_gen_4869
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 64
() -> length([nil, z]) -> 61
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 82
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 85
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 66
}
Sat witness: Found: ((length([ll, _yy])) -> length([cons(x, ll), s(_yy)]), {
_yy -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 65, which took 4.058428 s (model generation: 4.054924,  model checking: 0.003504):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4857
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 65
() -> length([nil, z]) -> 62
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 85
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 85
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 67
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(b, cons(b, cons(b, nil)))  ;  _dz -> s(s(s(z)))  ;  _ez -> cons(a, cons(b, cons(b, cons(b, cons(b, nil)))))  ;  _fz -> s(s(s(s(s(z)))))  ;  l1 -> cons(b, cons(b, cons(b, nil)))  ;  l2 -> cons(a, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 66, which took 4.634603 s (model generation: 4.627538,  model checking: 0.007065):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4865, q_gen_4871},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, a>() -> q_gen_4844
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4871
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<b, b, b>() -> q_gen_4855
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4857
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4857
<nil, cons, cons>(q_gen_4844, q_gen_4871) -> q_gen_4857
<a, a, a>() -> q_gen_4859
<a, b, a>() -> q_gen_4859
<b, a, b>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<cons, nil, cons>(q_gen_4844, q_gen_4871) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 66
() -> length([nil, z]) -> 63
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 85
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 88
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 68
}
Sat witness: Found: ((append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]), {
_ty -> cons(b, cons(b, cons(b, cons(b, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 67, which took 4.802669 s (model generation: 4.801959,  model checking: 0.000710):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4843, q_gen_4844, q_gen_4846, q_gen_4847, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4857, q_gen_4859, q_gen_4860, q_gen_4865},
Q_f={q_gen_4839},
Delta=
{
<nil>() -> q_gen_4853
<a>() -> q_gen_4854
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<a, b>() -> q_gen_4844
<b, a>() -> q_gen_4844
<b, b>() -> q_gen_4844
<cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4846
<cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4846
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4846
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4846
<a, a>() -> q_gen_4847
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4857) -> q_gen_4839
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<cons, nil, cons>(q_gen_4847, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4847, q_gen_4846) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4857) -> q_gen_4852
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4847, q_gen_4846) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4846) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<cons, nil, cons>(q_gen_4844, q_gen_4846) -> q_gen_4857
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 69
() -> length([nil, z]) -> 64
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 85
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 88
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 68
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 68, which took 3.027383 s (model generation: 3.020221,  model checking: 0.007162):

Model:
|_
{
append -> 
{{{
Q={q_gen_4839, q_gen_4842, q_gen_4843, q_gen_4844, q_gen_4847, q_gen_4852, q_gen_4853, q_gen_4854, q_gen_4855, q_gen_4858, q_gen_4859, q_gen_4860, q_gen_4862, q_gen_4865, q_gen_4882, q_gen_4883, q_gen_4889, q_gen_4890, q_gen_4891, q_gen_4901},
Q_f={q_gen_4839, q_gen_4842, q_gen_4882, q_gen_4889},
Delta=
{
<nil>() -> q_gen_4853
<b>() -> q_gen_4854
<cons>(q_gen_4854, q_gen_4853) -> q_gen_4865
<cons>(q_gen_4854, q_gen_4865) -> q_gen_4865
<a>() -> q_gen_4883
<cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4843
<cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4843
<nil, nil>() -> q_gen_4843
<b, b>() -> q_gen_4844
<a, a>() -> q_gen_4847
<a, b>() -> q_gen_4847
<b, a>() -> q_gen_4847
<nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4858
<nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4858
<cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4891
<cons, cons>(q_gen_4844, q_gen_4891) -> q_gen_4891
<nil, cons>(q_gen_4883, q_gen_4853) -> q_gen_4891
<cons, cons, cons>(q_gen_4855, q_gen_4852) -> q_gen_4839
<cons, cons, cons>(q_gen_4855, q_gen_4882) -> q_gen_4839
<nil, cons, cons>(q_gen_4844, q_gen_4843) -> q_gen_4839
<nil, cons, cons>(q_gen_4847, q_gen_4843) -> q_gen_4839
<nil, nil, nil>() -> q_gen_4839
<cons, cons, cons>(q_gen_4859, q_gen_4852) -> q_gen_4842
<cons, cons, cons>(q_gen_4859, q_gen_4862) -> q_gen_4842
<cons, cons, cons>(q_gen_4859, q_gen_4901) -> q_gen_4842
<cons, nil, cons>(q_gen_4844, q_gen_4843) -> q_gen_4842
<cons, cons, cons>(q_gen_4855, q_gen_4901) -> q_gen_4852
<cons, cons, cons>(q_gen_4859, q_gen_4860) -> q_gen_4852
<cons, nil, cons>(q_gen_4844, q_gen_4858) -> q_gen_4852
<cons, nil, cons>(q_gen_4847, q_gen_4891) -> q_gen_4852
<nil, cons, cons>(q_gen_4844, q_gen_4891) -> q_gen_4852
<nil, nil, cons>(q_gen_4854, q_gen_4853) -> q_gen_4852
<a, a, a>() -> q_gen_4855
<b, a, b>() -> q_gen_4855
<b, b, b>() -> q_gen_4855
<a, b, a>() -> q_gen_4859
<cons, cons, cons>(q_gen_4855, q_gen_4839) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4862) -> q_gen_4860
<nil, nil, cons>(q_gen_4854, q_gen_4865) -> q_gen_4860
<cons, cons, cons>(q_gen_4855, q_gen_4860) -> q_gen_4862
<cons, cons, cons>(q_gen_4859, q_gen_4882) -> q_gen_4862
<nil, cons, cons>(q_gen_4844, q_gen_4858) -> q_gen_4862
<cons, cons, cons>(q_gen_4855, q_gen_4842) -> q_gen_4882
<nil, cons, cons>(q_gen_4847, q_gen_4858) -> q_gen_4882
<nil, nil, cons>(q_gen_4883, q_gen_4853) -> q_gen_4882
<cons, cons, cons>(q_gen_4855, q_gen_4890) -> q_gen_4889
<cons, cons, cons>(q_gen_4859, q_gen_4890) -> q_gen_4889
<cons, cons, cons>(q_gen_4855, q_gen_4889) -> q_gen_4890
<cons, cons, cons>(q_gen_4859, q_gen_4842) -> q_gen_4890
<cons, nil, cons>(q_gen_4844, q_gen_4891) -> q_gen_4890
<cons, nil, cons>(q_gen_4847, q_gen_4843) -> q_gen_4890
<cons, cons, cons>(q_gen_4859, q_gen_4839) -> q_gen_4901
<nil, cons, cons>(q_gen_4847, q_gen_4891) -> q_gen_4901
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_4838, q_gen_4841},
Q_f={q_gen_4838},
Delta=
{
<a>() -> q_gen_4841
<b>() -> q_gen_4841
<cons, s>(q_gen_4841, q_gen_4838) -> q_gen_4838
<nil, z>() -> q_gen_4838
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 70
() -> length([nil, z]) -> 65
(append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]) -> 88
(append([t1, l2, _ty])) -> append([cons(h1, t1), l2, cons(h1, _ty)]) -> 88
(length([ll, _yy])) -> length([cons(x, ll), s(_yy)]) -> 69
}
Sat witness: Found: ((append([l1, l2, _cz]) /\ append([l2, l1, _ez]) /\ length([_cz, _dz]) /\ length([_ez, _fz])) -> eq_nat([_dz, _fz]), {
_cz -> cons(a, cons(b, cons(b, cons(a, nil))))  ;  _dz -> s(s(s(s(z))))  ;  _ez -> cons(b, cons(a, cons(a, cons(b, cons(b, nil)))))  ;  _fz -> s(s(s(s(s(z)))))  ;  l1 -> cons(a, cons(b, cons(b, cons(b, nil))))  ;  l2 -> cons(b, cons(a, cons(a, nil)))
})

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