Solving ../../benchmarks/true/list_delete_all_count.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}  ;  nat -> {s, z}
}
definition:
{
(delete_one, F:
{() -> delete_one([x, nil, nil])
() -> delete_one([y, cons(y, r), r])
(delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)])}
(delete_one([_ng, _og, _pg]) /\ delete_one([_ng, _og, _qg])) -> eq_eltlist([_pg, _qg])
)
(delete_all, F:
{() -> delete_all([x, nil, nil])
(delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)])
(delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg])}
(delete_all([_tg, _ug, _vg]) /\ delete_all([_tg, _ug, _wg])) -> eq_eltlist([_vg, _wg])
)
(leqnat, P:
{() -> leqnat([z, n2])
(leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)])
(leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2])
(leqnat([s(nn1), z])) -> BOT}
)
(count, F:
{() -> count([x, nil, z])
(count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg])
(count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)])}
(count([_zg, _ah, _bh]) /\ count([_zg, _ah, _ch])) -> eq_nat([_bh, _ch])
)
}

properties:
{(count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)])}


over-approximation: {count, delete_all, delete_one}
under-approximation: {leqnat}

Clause system for inference is:

{
() -> count([x, nil, z]) -> 0  ;  () -> delete_all([x, nil, nil]) -> 0  ;  () -> delete_one([x, nil, nil]) -> 0  ;  () -> delete_one([y, cons(y, r), r]) -> 0  ;  () -> leqnat([z, n2]) -> 0  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 0  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 0  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 0  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 0  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 0  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 0  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 0  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 0  ;  (leqnat([s(nn1), z])) -> BOT -> 0
}


Solving took 30.074121 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3938, q_gen_3939, q_gen_3940, q_gen_3941, q_gen_3942, q_gen_3943, q_gen_3952, q_gen_3963, q_gen_3964, q_gen_3965, q_gen_3966, q_gen_3982, q_gen_3983, q_gen_3984, q_gen_3985, q_gen_4000, q_gen_4001, q_gen_4002, q_gen_4003, q_gen_4004, q_gen_4005, q_gen_4006, q_gen_4007, q_gen_4008, q_gen_4009, q_gen_4022, q_gen_4023, q_gen_4024, q_gen_4025},
Q_f={},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3966
<cons>(q_gen_3966, q_gen_3942) -> q_gen_3985
<z>() -> q_gen_4003
<s>(q_gen_4003) -> q_gen_4025
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<a, z>() -> q_gen_3964
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3983
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_4001
<b, s>(q_gen_4003) -> q_gen_4002
<cons, s>(q_gen_3964, q_gen_3939) -> q_gen_4005
<cons, s>(q_gen_3940, q_gen_3983) -> q_gen_4007
<a, s>(q_gen_4003) -> q_gen_4008
<cons, s>(q_gen_4002, q_gen_4001) -> q_gen_4023
<b, s>(q_gen_4025) -> q_gen_4024
<b, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3938
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3941
<a, nil, z>() -> q_gen_3952
<a, cons, s>(q_gen_3964, q_gen_3939) -> q_gen_3963
<a, cons, z>(q_gen_3966, q_gen_3942) -> q_gen_3965
<b, cons, s>(q_gen_3940, q_gen_3983) -> q_gen_3982
<a, cons, z>(q_gen_3966, q_gen_3985) -> q_gen_3984
<b, cons, s>(q_gen_4002, q_gen_4001) -> q_gen_4000
<b, cons, s>(q_gen_4002, q_gen_4005) -> q_gen_4004
<b, cons, s>(q_gen_4008, q_gen_4007) -> q_gen_4006
<a, cons, s>(q_gen_4002, q_gen_4001) -> q_gen_4009
<b, cons, s>(q_gen_4024, q_gen_4023) -> q_gen_4022
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3930, q_gen_3931, q_gen_3932, q_gen_3933, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937, q_gen_3951, q_gen_3957, q_gen_3958, q_gen_3959, q_gen_3960, q_gen_3961, q_gen_3962, q_gen_3975, q_gen_3976, q_gen_3977, q_gen_3978, q_gen_3979, q_gen_3980, q_gen_3981, q_gen_3993, q_gen_3994, q_gen_3995, q_gen_3996, q_gen_3997, q_gen_3998, q_gen_3999, q_gen_4010, q_gen_4018, q_gen_4019, q_gen_4020, q_gen_4021, q_gen_4026, q_gen_4041, q_gen_4042, q_gen_4043, q_gen_4044, q_gen_4045},
Q_f={},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<a>() -> q_gen_3958
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3977
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<nil, b>() -> q_gen_3960
<b, nil>() -> q_gen_3961
<b, b>() -> q_gen_3962
<cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3980
<cons, a>(q_gen_3958, q_gen_3931) -> q_gen_3981
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3994
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3995
<a, b>() -> q_gen_3996
<cons, cons>(q_gen_3962, q_gen_3961, q_gen_3960, q_gen_3934) -> q_gen_3998
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3999
<b, a>() -> q_gen_4019
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_4021
<cons, cons>(q_gen_3962, q_gen_3961, q_gen_3995, q_gen_3994) -> q_gen_4042
<cons, b>(q_gen_3932, q_gen_3977) -> q_gen_4043
<a, cons>(q_gen_3932, q_gen_3931) -> q_gen_4044
<b, nil, nil>() -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3930
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3933
<a, nil, nil>() -> q_gen_3951
<a, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3957
<a, cons, cons>(q_gen_3962, q_gen_3961, q_gen_3960, q_gen_3934) -> q_gen_3959
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3975
<a, cons, nil>(q_gen_3958, q_gen_3977) -> q_gen_3976
<b, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3978
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3981, q_gen_3980) -> q_gen_3979
<a, cons, cons>(q_gen_3996, q_gen_3936, q_gen_3995, q_gen_3994) -> q_gen_3993
<a, cons, cons>(q_gen_3962, q_gen_3999, q_gen_3995, q_gen_3998) -> q_gen_3997
<a, cons, nil>(q_gen_3932, q_gen_3977) -> q_gen_4010
<b, cons, cons>(q_gen_4019, q_gen_3961, q_gen_3981, q_gen_3980) -> q_gen_4018
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_4021, q_gen_3994) -> q_gen_4020
<b, cons, nil>(q_gen_3932, q_gen_3977) -> q_gen_4026
<a, cons, cons>(q_gen_3996, q_gen_4044, q_gen_4043, q_gen_4042) -> q_gen_4041
<a, cons, cons>(q_gen_4019, q_gen_3961, q_gen_4021, q_gen_3994) -> q_gen_4045
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3921, q_gen_3925, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3948, q_gen_3949, q_gen_3950, q_gen_3953, q_gen_3954, q_gen_3955, q_gen_3956, q_gen_3967, q_gen_3968, q_gen_3969, q_gen_3970, q_gen_3971, q_gen_3972, q_gen_3973, q_gen_3974, q_gen_3986, q_gen_3987, q_gen_3988, q_gen_3989, q_gen_3990, q_gen_3991, q_gen_3992, q_gen_4011, q_gen_4014, q_gen_4015, q_gen_4016, q_gen_4017, q_gen_4027, q_gen_4028, q_gen_4029, q_gen_4030, q_gen_4031, q_gen_4032, q_gen_4033, q_gen_4034, q_gen_4035, q_gen_4036, q_gen_4037, q_gen_4038, q_gen_4039, q_gen_4040, q_gen_4046},
Q_f={},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<a>() -> q_gen_3949
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3991
<cons>(q_gen_3949, q_gen_3991) -> q_gen_4033
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<nil, b>() -> q_gen_3954
<b, nil>() -> q_gen_3955
<b, b>() -> q_gen_3956
<cons, nil>(q_gen_3949, q_gen_3919) -> q_gen_3968
<cons, a>(q_gen_3949, q_gen_3919) -> q_gen_3969
<b, a>() -> q_gen_3970
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3973
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3974
<a, b>() -> q_gen_3987
<cons, cons>(q_gen_3956, q_gen_3955, q_gen_3974, q_gen_3973) -> q_gen_3989
<cons, b>(q_gen_3920, q_gen_3991) -> q_gen_3990
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3992
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_4015
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_4017
<cons, cons>(q_gen_3970, q_gen_3992, q_gen_4031, q_gen_4030) -> q_gen_4029
<cons, cons>(q_gen_3987, q_gen_3928, q_gen_3974, q_gen_3973) -> q_gen_4030
<cons, a>(q_gen_3949, q_gen_3991) -> q_gen_4031
<cons, b>(q_gen_3920, q_gen_4033) -> q_gen_4032
<b, cons>(q_gen_3949, q_gen_3991) -> q_gen_4034
<cons, cons>(q_gen_3956, q_gen_3955, q_gen_3954, q_gen_3926) -> q_gen_4036
<cons, cons>(q_gen_3956, q_gen_3992, q_gen_3974, q_gen_4036) -> q_gen_4038
<cons, a>(q_gen_3920, q_gen_3991) -> q_gen_4039
<a, cons>(q_gen_3920, q_gen_3991) -> q_gen_4040
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3921
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3925
<a, cons, nil>(q_gen_3949, q_gen_3919) -> q_gen_3948
<a, nil, nil>() -> q_gen_3950
<a, cons, cons>(q_gen_3956, q_gen_3955, q_gen_3954, q_gen_3926) -> q_gen_3953
<b, cons, cons>(q_gen_3970, q_gen_3955, q_gen_3969, q_gen_3968) -> q_gen_3967
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3971
<a, cons, cons>(q_gen_3956, q_gen_3955, q_gen_3974, q_gen_3973) -> q_gen_3972
<a, cons, cons>(q_gen_3987, q_gen_3928, q_gen_3974, q_gen_3973) -> q_gen_3986
<a, cons, cons>(q_gen_3956, q_gen_3992, q_gen_3990, q_gen_3989) -> q_gen_3988
<a, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
<a, cons, cons>(q_gen_3987, q_gen_4015, q_gen_3990, q_gen_3989) -> q_gen_4014
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_4017, q_gen_3973) -> q_gen_4016
<b, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4027
<b, cons, cons>(q_gen_3956, q_gen_4034, q_gen_4032, q_gen_4029) -> q_gen_4028
<b, cons, cons>(q_gen_3956, q_gen_3992, q_gen_3974, q_gen_4036) -> q_gen_4035
<b, cons, cons>(q_gen_3929, q_gen_4040, q_gen_4039, q_gen_4038) -> q_gen_4037
<a, cons, cons>(q_gen_3970, q_gen_3955, q_gen_4017, q_gen_3973) -> q_gen_4046
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3924, q_gen_3944, q_gen_3945, q_gen_3946, q_gen_3947, q_gen_4012, q_gen_4013},
Q_f={},
Delta=
{
<z>() -> q_gen_3945
<s>(q_gen_3945) -> q_gen_3947
<z, z>() -> q_gen_3917
<s, s>(q_gen_3917) -> q_gen_3924
<z, s>(q_gen_3945) -> q_gen_3944
<z, s>(q_gen_3947) -> q_gen_3946
<s, s>(q_gen_4013) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4013
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007679 s (model generation: 0.007006,  model checking: 0.000673):

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

}

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

}

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

}

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

}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0  ;  () -> delete_all([x, nil, nil]) -> 0  ;  () -> delete_one([x, nil, nil]) -> 0  ;  () -> delete_one([y, cons(y, r), r]) -> 0  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> leqnat([z, n2]), {
n2 -> z
})

-------------------------------------------
Step 1, which took 0.007202 s (model generation: 0.006816,  model checking: 0.000386):

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

}

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

}

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0  ;  () -> delete_all([x, nil, nil]) -> 0  ;  () -> delete_one([x, nil, nil]) -> 0  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> delete_one([y, cons(y, r), r]), {
r -> nil  ;  y -> b
})

-------------------------------------------
Step 2, which took 0.011270 s (model generation: 0.010685,  model checking: 0.000585):

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

}

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0  ;  () -> delete_all([x, nil, nil]) -> 0  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> delete_one([x, nil, nil]), {
x -> b
})

-------------------------------------------
Step 3, which took 0.011421 s (model generation: 0.010816,  model checking: 0.000605):

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

}

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

}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 0  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> delete_all([x, nil, nil]), {
x -> b
})

-------------------------------------------
Step 4, which took 0.006488 s (model generation: 0.006258,  model checking: 0.000230):

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

}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922},
Q_f={q_gen_3922},
Delta=
{
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 1  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 1  ;  (leqnat([s(nn1), z])) -> BOT -> 1
}
Sat witness: Yes: (() -> count([x, nil, z]), {
x -> b
})

-------------------------------------------
Step 5, which took 0.010947 s (model generation: 0.010884,  model checking: 0.000063):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923},
Q_f={q_gen_3923},
Delta=
{
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922},
Q_f={q_gen_3922},
Delta=
{
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 1  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 6, which took 0.003800 s (model generation: 0.003576,  model checking: 0.000224):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923},
Q_f={q_gen_3923},
Delta=
{
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922},
Q_f={q_gen_3922},
Delta=
{
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<s, s>(q_gen_3917) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 1  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]), {
_mg -> nil  ;  r -> nil  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 7, which took 0.011766 s (model generation: 0.011439,  model checking: 0.000327):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923},
Q_f={q_gen_3923},
Delta=
{
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922},
Q_f={q_gen_3922},
Delta=
{
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<s, s>(q_gen_3917) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 1  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]), {
_rg -> nil  ;  r -> nil  ;  y -> b
})

-------------------------------------------
Step 8, which took 0.012361 s (model generation: 0.011780,  model checking: 0.000581):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923},
Q_f={q_gen_3923},
Delta=
{
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<s, s>(q_gen_3917) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 1  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]), {
_sg -> nil  ;  r -> nil  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 9, which took 0.014787 s (model generation: 0.014522,  model checking: 0.000265):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923},
Q_f={q_gen_3923},
Delta=
{
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<s, s>(q_gen_3917) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 1  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]), {
_xg -> z  ;  r -> nil  ;  y -> b
})

-------------------------------------------
Step 10, which took 0.013182 s (model generation: 0.012698,  model checking: 0.000484):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940},
Q_f={q_gen_3923},
Delta=
{
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<s, s>(q_gen_3917) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 1  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]), {
_yg -> z  ;  r -> nil  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 11, which took 0.012312 s (model generation: 0.012205,  model checking: 0.000107):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917},
Q_f={q_gen_3917},
Delta=
{
<s, s>(q_gen_3917) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 3  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 2  ;  (leqnat([s(nn1), z])) -> BOT -> 2
}
Sat witness: Yes: ((count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]), {
_eh -> nil  ;  _fh -> z  ;  l -> nil  ;  x -> b
})

-------------------------------------------
Step 12, which took 0.007759 s (model generation: 0.007416,  model checking: 0.000343):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 3  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 3  ;  (leqnat([s(nn1), z])) -> BOT -> 3
}
Sat witness: Yes: (() -> leqnat([z, n2]), {
n2 -> s(s(z))
})

-------------------------------------------
Step 13, which took 0.015489 s (model generation: 0.013704,  model checking: 0.001785):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 3  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4  ;  (leqnat([s(nn1), z])) -> BOT -> 4
}
Sat witness: Yes: (() -> delete_one([y, cons(y, r), r]), {
r -> nil  ;  y -> a
})

-------------------------------------------
Step 14, which took 0.014942 s (model generation: 0.013993,  model checking: 0.000949):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 3  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4  ;  (leqnat([s(nn1), z])) -> BOT -> 4
}
Sat witness: Yes: (() -> delete_one([x, nil, nil]), {
x -> a
})

-------------------------------------------
Step 15, which took 0.015133 s (model generation: 0.014199,  model checking: 0.000934):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 3  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4  ;  (leqnat([s(nn1), z])) -> BOT -> 4
}
Sat witness: Yes: (() -> delete_all([x, nil, nil]), {
x -> a
})

-------------------------------------------
Step 16, which took 0.014782 s (model generation: 0.014355,  model checking: 0.000427):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 4  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 4  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 4  ;  (leqnat([s(nn1), z])) -> BOT -> 4
}
Sat witness: Yes: (() -> count([x, nil, z]), {
x -> a
})

-------------------------------------------
Step 17, which took 0.019520 s (model generation: 0.015004,  model checking: 0.004516):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 4  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 7  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5  ;  (leqnat([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]), {
_mg -> nil  ;  r -> nil  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 18, which took 0.017437 s (model generation: 0.015343,  model checking: 0.002094):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 4  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 7  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 7  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5  ;  (leqnat([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]), {
_rg -> nil  ;  r -> nil  ;  y -> a
})

-------------------------------------------
Step 19, which took 0.019786 s (model generation: 0.015570,  model checking: 0.004216):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 4  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 7  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 7  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 7  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5  ;  (leqnat([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]), {
_sg -> nil  ;  r -> nil  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 20, which took 0.016811 s (model generation: 0.016092,  model checking: 0.000719):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<b, z>() -> q_gen_3940
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 4  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 7  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 7  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 7  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 7  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5  ;  (leqnat([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]), {
_xg -> z  ;  r -> nil  ;  y -> a
})

-------------------------------------------
Step 21, which took 0.016417 s (model generation: 0.015725,  model checking: 0.000692):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 6  ;  () -> leqnat([z, n2]) -> 6  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 4  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 7  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 7  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 7  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 7  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 7  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 5  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 5  ;  (leqnat([s(nn1), z])) -> BOT -> 5
}
Sat witness: Yes: ((count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]), {
_yg -> z  ;  r -> nil  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 22, which took 0.022252 s (model generation: 0.015351,  model checking: 0.006901):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<nil, nil>() -> q_gen_3926
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 6  ;  () -> delete_all([x, nil, nil]) -> 6  ;  () -> delete_one([x, nil, nil]) -> 6  ;  () -> delete_one([y, cons(y, r), r]) -> 9  ;  () -> leqnat([z, n2]) -> 7  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 5  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 7  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 7  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 7  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 7  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 7  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 6  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 6  ;  (leqnat([s(nn1), z])) -> BOT -> 6
}
Sat witness: Yes: (() -> delete_one([y, cons(y, r), r]), {
r -> cons(a, nil)  ;  y -> b
})

-------------------------------------------
Step 23, which took 0.025477 s (model generation: 0.017669,  model checking: 0.007808):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7  ;  () -> delete_all([x, nil, nil]) -> 7  ;  () -> delete_one([x, nil, nil]) -> 7  ;  () -> delete_one([y, cons(y, r), r]) -> 9  ;  () -> leqnat([z, n2]) -> 7  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 6  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 7  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 7  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 7  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 7  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 10  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 7  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 7  ;  (leqnat([s(nn1), z])) -> BOT -> 7
}
Sat witness: Yes: ((delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]), {
_mg -> nil  ;  r -> cons(b, nil)  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 24, which took 0.022950 s (model generation: 0.019641,  model checking: 0.003309):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7  ;  () -> delete_all([x, nil, nil]) -> 7  ;  () -> delete_one([x, nil, nil]) -> 7  ;  () -> delete_one([y, cons(y, r), r]) -> 9  ;  () -> leqnat([z, n2]) -> 7  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 7  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 7  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 7  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 7  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 10  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 10  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 8  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 8  ;  (leqnat([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]), {
_rg -> nil  ;  r -> cons(b, nil)  ;  y -> a
})

-------------------------------------------
Step 25, which took 0.026823 s (model generation: 0.021120,  model checking: 0.005703):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<nil, nil>() -> q_gen_3934
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7  ;  () -> delete_all([x, nil, nil]) -> 7  ;  () -> delete_one([x, nil, nil]) -> 7  ;  () -> delete_one([y, cons(y, r), r]) -> 9  ;  () -> leqnat([z, n2]) -> 7  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 7  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 7  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 7  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 10  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 10  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 10  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 8  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 8  ;  (leqnat([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]), {
_sg -> nil  ;  r -> cons(a, nil)  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 26, which took 0.023181 s (model generation: 0.022436,  model checking: 0.000745):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7  ;  () -> delete_all([x, nil, nil]) -> 7  ;  () -> delete_one([x, nil, nil]) -> 7  ;  () -> delete_one([y, cons(y, r), r]) -> 9  ;  () -> leqnat([z, n2]) -> 7  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 7  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 7  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 10  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 10  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 10  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 10  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 8  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 8  ;  (leqnat([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]), {
_xg -> z  ;  r -> cons(a, nil)  ;  y -> b
})

-------------------------------------------
Step 27, which took 0.022882 s (model generation: 0.022156,  model checking: 0.000726):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 7  ;  () -> delete_all([x, nil, nil]) -> 7  ;  () -> delete_one([x, nil, nil]) -> 7  ;  () -> delete_one([y, cons(y, r), r]) -> 9  ;  () -> leqnat([z, n2]) -> 7  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 7  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 10  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 10  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 10  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 10  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 10  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 8  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 8  ;  (leqnat([s(nn1), z])) -> BOT -> 8
}
Sat witness: Yes: ((count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]), {
_yg -> z  ;  r -> cons(b, nil)  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 28, which took 0.035074 s (model generation: 0.021438,  model checking: 0.013636):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 8  ;  () -> delete_all([x, nil, nil]) -> 8  ;  () -> delete_one([x, nil, nil]) -> 8  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 8  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 8  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 10  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 10  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 10  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 10  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 10  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 9  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 9  ;  (leqnat([s(nn1), z])) -> BOT -> 9
}
Sat witness: Yes: (() -> delete_one([y, cons(y, r), r]), {
r -> cons(b, nil)  ;  y -> a
})

-------------------------------------------
Step 29, which took 0.029280 s (model generation: 0.019665,  model checking: 0.009615):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 9  ;  () -> delete_all([x, nil, nil]) -> 9  ;  () -> delete_one([x, nil, nil]) -> 9  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 9  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 9  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 10  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 10  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 10  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 10  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 10  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 10  ;  (leqnat([s(nn1), z])) -> BOT -> 10
}
Sat witness: Yes: ((delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]), {
_mg -> cons(b, nil)  ;  r -> cons(b, cons(b, nil))  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 30, which took 0.023610 s (model generation: 0.019636,  model checking: 0.003974):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 10  ;  () -> delete_all([x, nil, nil]) -> 10  ;  () -> delete_one([x, nil, nil]) -> 10  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 10  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 10  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 10  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 10  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 10  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11  ;  (leqnat([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]), {
_rg -> cons(b, nil)  ;  r -> cons(b, nil)  ;  y -> a
})

-------------------------------------------
Step 31, which took 0.028720 s (model generation: 0.025747,  model checking: 0.002973):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 10  ;  () -> delete_all([x, nil, nil]) -> 10  ;  () -> delete_one([x, nil, nil]) -> 10  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 10  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 10  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 10  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 10  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11  ;  (leqnat([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]), {
_sg -> cons(b, nil)  ;  r -> cons(b, nil)  ;  x -> a  ;  y -> b
})

-------------------------------------------
Step 32, which took 0.025082 s (model generation: 0.024170,  model checking: 0.000912):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 10  ;  () -> delete_all([x, nil, nil]) -> 10  ;  () -> delete_one([x, nil, nil]) -> 10  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 10  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 10  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 10  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11  ;  (leqnat([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]), {
_xg -> s(z)  ;  r -> cons(b, nil)  ;  y -> b
})

-------------------------------------------
Step 33, which took 0.014013 s (model generation: 0.013433,  model checking: 0.000580):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 10  ;  () -> delete_all([x, nil, nil]) -> 10  ;  () -> delete_one([x, nil, nil]) -> 10  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 10  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 10  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11  ;  (leqnat([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]), {
_yg -> s(s(z))  ;  r -> cons(b, cons(a, nil))  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 34, which took 0.014179 s (model generation: 0.013778,  model checking: 0.000401):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 10  ;  () -> delete_all([x, nil, nil]) -> 10  ;  () -> delete_one([x, nil, nil]) -> 10  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 10  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11  ;  (leqnat([s(nn1), z])) -> BOT -> 11
}
Sat witness: Yes: ((count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]), {
_eh -> nil  ;  _fh -> s(s(z))  ;  l -> cons(b, cons(b, nil))  ;  x -> a
})

-------------------------------------------
Step 35, which took 0.020273 s (model generation: 0.019637,  model checking: 0.000636):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<s, z>(q_gen_3945) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 11  ;  () -> delete_all([x, nil, nil]) -> 11  ;  () -> delete_one([x, nil, nil]) -> 11  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 11  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 11  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((leqnat([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 36, which took 0.015238 s (model generation: 0.015109,  model checking: 0.000129):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4013},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<s, s>(q_gen_4013) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, z>(q_gen_3945) -> q_gen_4013
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 11  ;  () -> delete_all([x, nil, nil]) -> 11  ;  () -> delete_one([x, nil, nil]) -> 11  ;  () -> delete_one([y, cons(y, r), r]) -> 12  ;  () -> leqnat([z, n2]) -> 11  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 11  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 37, which took 0.016426 s (model generation: 0.015063,  model checking: 0.001363):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937, q_gen_3958, q_gen_3975},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<a>() -> q_gen_3958
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3958, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3975
<b, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3975
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 12  ;  () -> delete_all([x, nil, nil]) -> 12  ;  () -> delete_one([x, nil, nil]) -> 12  ;  () -> delete_one([y, cons(y, r), r]) -> 15  ;  () -> leqnat([z, n2]) -> 12  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 13  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 12  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: (() -> delete_one([y, cons(y, r), r]), {
r -> cons(b, cons(b, nil))  ;  y -> a
})

-------------------------------------------
Step 38, which took 0.026586 s (model generation: 0.024317,  model checking: 0.002269):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3949, q_gen_3971},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<a>() -> q_gen_3949
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<cons, nil>(q_gen_3949, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3949, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3949, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3971
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 13  ;  () -> delete_all([x, nil, nil]) -> 13  ;  () -> delete_one([x, nil, nil]) -> 13  ;  () -> delete_one([y, cons(y, r), r]) -> 15  ;  () -> leqnat([z, n2]) -> 13  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 13  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 16  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 13  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]), {
_mg -> nil  ;  r -> cons(b, nil)  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 39, which took 0.025707 s (model generation: 0.024953,  model checking: 0.000754):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3991, q_gen_4011},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3991
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3991) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 13  ;  () -> delete_all([x, nil, nil]) -> 13  ;  () -> delete_one([x, nil, nil]) -> 13  ;  () -> delete_one([y, cons(y, r), r]) -> 15  ;  () -> leqnat([z, n2]) -> 13  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 13  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 16  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 16  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 14  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]), {
_rg -> cons(a, nil)  ;  r -> cons(a, nil)  ;  y -> b
})

-------------------------------------------
Step 40, which took 0.020832 s (model generation: 0.019581,  model checking: 0.001251):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937, q_gen_3958, q_gen_3975},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<a>() -> q_gen_3958
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3958, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3975
<b, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3975
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 13  ;  () -> delete_all([x, nil, nil]) -> 13  ;  () -> delete_one([x, nil, nil]) -> 13  ;  () -> delete_one([y, cons(y, r), r]) -> 15  ;  () -> leqnat([z, n2]) -> 13  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 13  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 16  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 16  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 16  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 14  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]), {
_sg -> nil  ;  r -> cons(b, nil)  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 41, which took 0.024304 s (model generation: 0.022047,  model checking: 0.002257):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3949, q_gen_3971},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<b>() -> q_gen_3920
<a>() -> q_gen_3949
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<cons, nil>(q_gen_3949, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, a>(q_gen_3949, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3949, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3971
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 13  ;  () -> delete_all([x, nil, nil]) -> 13  ;  () -> delete_one([x, nil, nil]) -> 13  ;  () -> delete_one([y, cons(y, r), r]) -> 15  ;  () -> leqnat([z, n2]) -> 13  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 13  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 13  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 16  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 16  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 16  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 16  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 14  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]), {
_xg -> s(s(z))  ;  r -> cons(b, cons(b, nil))  ;  y -> b
})

-------------------------------------------
Step 42, which took 0.021819 s (model generation: 0.021317,  model checking: 0.000502):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<s>(q_gen_4003) -> q_gen_4003
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937, q_gen_3958, q_gen_3975},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<b>() -> q_gen_3932
<a>() -> q_gen_3958
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, a>(q_gen_3958, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3975
<b, cons, nil>(q_gen_3958, q_gen_3931) -> q_gen_3975
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929},
Q_f={q_gen_3918},
Delta=
{
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3919
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 13  ;  () -> delete_all([x, nil, nil]) -> 13  ;  () -> delete_one([x, nil, nil]) -> 13  ;  () -> delete_one([y, cons(y, r), r]) -> 15  ;  () -> leqnat([z, n2]) -> 13  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 16  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 14  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 16  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 16  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 16  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 16  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 14  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 14  ;  (leqnat([s(nn1), z])) -> BOT -> 14
}
Sat witness: Yes: ((count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]), {
_eh -> nil  ;  _fh -> s(s(z))  ;  l -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 43, which took 0.083355 s (model generation: 0.018426,  model checking: 0.064929):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<s>(q_gen_4003) -> q_gen_4003
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3991, q_gen_4011},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3991
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3991) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
<b, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 14  ;  () -> delete_all([x, nil, nil]) -> 14  ;  () -> delete_one([x, nil, nil]) -> 14  ;  () -> delete_one([y, cons(y, r), r]) -> 18  ;  () -> leqnat([z, n2]) -> 14  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 16  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 15  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 16  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 16  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 16  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 16  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 15  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 15  ;  (leqnat([s(nn1), z])) -> BOT -> 15
}
Sat witness: Yes: (() -> delete_one([y, cons(y, r), r]), {
r -> cons(b, cons(a, cons(b, nil)))  ;  y -> b
})

-------------------------------------------
Step 44, which took 0.076473 s (model generation: 0.020312,  model checking: 0.056161):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<s>(q_gen_4003) -> q_gen_4003
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3991, q_gen_4011},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3991
<cons>(q_gen_3920, q_gen_3991) -> q_gen_3991
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, a>(q_gen_3920, q_gen_3991) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3991) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3991) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
<b, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 15  ;  () -> delete_all([x, nil, nil]) -> 15  ;  () -> delete_one([x, nil, nil]) -> 15  ;  () -> delete_one([y, cons(y, r), r]) -> 18  ;  () -> leqnat([z, n2]) -> 15  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 16  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 16  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 16  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 16  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 16  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 19  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 16  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 16  ;  (leqnat([s(nn1), z])) -> BOT -> 16
}
Sat witness: Yes: ((delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]), {
_mg -> cons(b, cons(b, nil))  ;  r -> cons(b, cons(b, nil))  ;  x -> b  ;  y -> a
})

-------------------------------------------
Step 45, which took 0.023263 s (model generation: 0.021364,  model checking: 0.001899):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<s>(q_gen_4003) -> q_gen_4003
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3991, q_gen_4011},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3991
<cons>(q_gen_3920, q_gen_3991) -> q_gen_3991
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, a>(q_gen_3920, q_gen_3991) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3991) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, cons>(q_gen_3920, q_gen_3991) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3991) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
<b, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 16  ;  () -> delete_all([x, nil, nil]) -> 16  ;  () -> delete_one([x, nil, nil]) -> 16  ;  () -> delete_one([y, cons(y, r), r]) -> 18  ;  () -> leqnat([z, n2]) -> 16  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 16  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 16  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 16  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 16  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 19  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 19  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 17  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 17  ;  (leqnat([s(nn1), z])) -> BOT -> 17
}
Sat witness: Yes: ((delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]), {
_rg -> cons(b, cons(b, nil))  ;  r -> cons(b, cons(b, nil))  ;  y -> a
})

-------------------------------------------
Step 46, which took 0.030658 s (model generation: 0.022826,  model checking: 0.007832):

Model:
|_
{
count -> 
{{{
Q={q_gen_3923, q_gen_3939, q_gen_3940, q_gen_3942, q_gen_3943, q_gen_4003},
Q_f={q_gen_3923},
Delta=
{
<cons>(q_gen_3943, q_gen_3942) -> q_gen_3942
<nil>() -> q_gen_3942
<a>() -> q_gen_3943
<b>() -> q_gen_3943
<s>(q_gen_4003) -> q_gen_4003
<z>() -> q_gen_4003
<cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3939
<cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3939
<nil, z>() -> q_gen_3939
<a, s>(q_gen_4003) -> q_gen_3940
<a, z>() -> q_gen_3940
<b, s>(q_gen_4003) -> q_gen_3940
<b, z>() -> q_gen_3940
<a, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<a, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<a, nil, z>() -> q_gen_3923
<b, cons, s>(q_gen_3940, q_gen_3939) -> q_gen_3923
<b, cons, z>(q_gen_3943, q_gen_3942) -> q_gen_3923
<b, nil, z>() -> q_gen_3923
}

Datatype: <elt, eltlist, nat>
Convolution form: complete
}}}
  ;  delete_all -> 
{{{
Q={q_gen_3922, q_gen_3931, q_gen_3932, q_gen_3934, q_gen_3935, q_gen_3936, q_gen_3937},
Q_f={q_gen_3922},
Delta=
{
<cons>(q_gen_3932, q_gen_3931) -> q_gen_3931
<nil>() -> q_gen_3931
<a>() -> q_gen_3932
<b>() -> q_gen_3932
<cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3934
<cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3934
<nil, nil>() -> q_gen_3934
<cons, a>(q_gen_3932, q_gen_3931) -> q_gen_3935
<cons, b>(q_gen_3932, q_gen_3931) -> q_gen_3935
<nil, a>() -> q_gen_3935
<nil, b>() -> q_gen_3935
<a, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<a, nil>() -> q_gen_3936
<b, cons>(q_gen_3932, q_gen_3931) -> q_gen_3936
<b, nil>() -> q_gen_3936
<a, a>() -> q_gen_3937
<a, b>() -> q_gen_3937
<b, a>() -> q_gen_3937
<b, b>() -> q_gen_3937
<a, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<a, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<a, nil, nil>() -> q_gen_3922
<b, cons, cons>(q_gen_3937, q_gen_3936, q_gen_3935, q_gen_3934) -> q_gen_3922
<b, cons, nil>(q_gen_3932, q_gen_3931) -> q_gen_3922
<b, nil, nil>() -> q_gen_3922
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  delete_one -> 
{{{
Q={q_gen_3918, q_gen_3919, q_gen_3920, q_gen_3926, q_gen_3927, q_gen_3928, q_gen_3929, q_gen_3991, q_gen_4011},
Q_f={q_gen_3918},
Delta=
{
<nil>() -> q_gen_3919
<a>() -> q_gen_3920
<b>() -> q_gen_3920
<cons>(q_gen_3920, q_gen_3919) -> q_gen_3991
<cons>(q_gen_3920, q_gen_3991) -> q_gen_3991
<cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3926
<cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3926
<nil, nil>() -> q_gen_3926
<cons, a>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, a>(q_gen_3920, q_gen_3991) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3919) -> q_gen_3927
<cons, b>(q_gen_3920, q_gen_3991) -> q_gen_3927
<nil, a>() -> q_gen_3927
<nil, b>() -> q_gen_3927
<a, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<a, cons>(q_gen_3920, q_gen_3991) -> q_gen_3928
<a, nil>() -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3919) -> q_gen_3928
<b, cons>(q_gen_3920, q_gen_3991) -> q_gen_3928
<b, nil>() -> q_gen_3928
<a, a>() -> q_gen_3929
<a, b>() -> q_gen_3929
<b, a>() -> q_gen_3929
<b, b>() -> q_gen_3929
<a, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<a, nil, nil>() -> q_gen_3918
<b, cons, cons>(q_gen_3929, q_gen_3928, q_gen_3927, q_gen_3926) -> q_gen_3918
<b, cons, nil>(q_gen_3920, q_gen_3919) -> q_gen_3918
<b, nil, nil>() -> q_gen_3918
<a, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
<b, cons, nil>(q_gen_3920, q_gen_3991) -> q_gen_4011
}

Datatype: <elt, eltlist, eltlist>
Convolution form: complete
}}}
  ;  leqnat -> 
{{{
Q={q_gen_3917, q_gen_3945, q_gen_4012},
Q_f={q_gen_3917},
Delta=
{
<s>(q_gen_3945) -> q_gen_3945
<z>() -> q_gen_3945
<s, s>(q_gen_3917) -> q_gen_3917
<z, s>(q_gen_3945) -> q_gen_3917
<z, z>() -> q_gen_3917
<s, s>(q_gen_4012) -> q_gen_4012
<s, z>(q_gen_3945) -> q_gen_4012
}

Datatype: <nat, nat>
Convolution form: complete
}}}

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

Teacher's answer:
New clause system:
{
() -> count([x, nil, z]) -> 16  ;  () -> delete_all([x, nil, nil]) -> 16  ;  () -> delete_one([x, nil, nil]) -> 16  ;  () -> delete_one([y, cons(y, r), r]) -> 18  ;  () -> leqnat([z, n2]) -> 16  ;  (count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]) -> 19  ;  (count([x, r, _yg]) /\ not eq_elt([x, y])) -> count([x, cons(y, r), _yg]) -> 17  ;  (count([y, r, _xg])) -> count([y, cons(y, r), s(_xg)]) -> 17  ;  (delete_all([x, r, _sg]) /\ not eq_elt([x, y])) -> delete_all([x, cons(y, r), cons(y, _sg)]) -> 17  ;  (delete_all([y, r, _rg])) -> delete_all([y, cons(y, r), _rg]) -> 19  ;  (delete_one([x, r, _mg]) /\ not eq_elt([x, y])) -> delete_one([x, cons(y, r), cons(y, _mg)]) -> 19  ;  (leqnat([nn1, nn2])) -> leqnat([s(nn1), s(nn2)]) -> 17  ;  (leqnat([s(nn1), s(nn2)])) -> leqnat([nn1, nn2]) -> 17  ;  (leqnat([s(nn1), z])) -> BOT -> 17
}
Sat witness: Yes: ((count([x, l, _fh]) /\ delete_all([x, l, _eh]) /\ delete_one([x, l, _eh])) -> leqnat([_fh, s(z)]), {
_eh -> cons(a, nil)  ;  _fh -> s(s(z))  ;  l -> cons(b, cons(b, nil))  ;  x -> a
})

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