Solving ../../benchmarks/true/length_append_cons.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:
{
(le, P:
{() -> le([z, s(nn2)])
(le([nn1, nn2])) -> le([s(nn1), s(nn2)])
(le([s(nn1), s(nn2)])) -> le([nn1, nn2])
(le([s(nn1), z])) -> BOT
(le([z, z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _es])) -> length([cons(x, ll), s(_es)])}
(length([_fs, _gs]) /\ length([_fs, _hs])) -> eq_nat([_gs, _hs])
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)])}
(append([_js, _ks, _ls]) /\ append([_js, _ks, _ms])) -> eq_eltlist([_ls, _ms])
)
}

properties:
{(append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0  ;  () -> le([z, s(nn2)]) -> 0  ;  () -> length([nil, z]) -> 0  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 0  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 0  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 0  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 0  ;  (le([s(nn1), z])) -> BOT -> 0  ;  (le([z, z])) -> BOT -> 0  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 0
}


Solving took 30.006805 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2928, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2935, q_gen_2936, q_gen_2937, q_gen_2938, q_gen_2941, q_gen_2942, q_gen_2943, q_gen_2944, q_gen_2945, q_gen_2946, q_gen_2947, q_gen_2948, q_gen_2949, q_gen_2950, q_gen_2951, q_gen_2952, q_gen_2956, q_gen_2957, q_gen_2958, q_gen_2959, q_gen_2960, q_gen_2961, q_gen_2962, q_gen_2963, q_gen_2966, q_gen_2967, q_gen_2968, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975, q_gen_2980, q_gen_2981, q_gen_2982, q_gen_2983, q_gen_2984, q_gen_2985, q_gen_2986, q_gen_2987, q_gen_2988, q_gen_2989, q_gen_2990, q_gen_2991, q_gen_2992, q_gen_2993, q_gen_2994, q_gen_2995, q_gen_2996, q_gen_2997, q_gen_2998, q_gen_2999, q_gen_3000, q_gen_3001, q_gen_3002, q_gen_3003, q_gen_3004, q_gen_3005, q_gen_3006, q_gen_3007, q_gen_3008, q_gen_3009, q_gen_3010, q_gen_3011, q_gen_3012, q_gen_3013, q_gen_3014, q_gen_3015, q_gen_3016, q_gen_3017, q_gen_3018, q_gen_3019, q_gen_3020, q_gen_3021, q_gen_3022, q_gen_3023, q_gen_3024, q_gen_3025, q_gen_3026, q_gen_3027, q_gen_3028, q_gen_3029, q_gen_3030, q_gen_3031, q_gen_3032, q_gen_3033, q_gen_3034, q_gen_3035, q_gen_3036, q_gen_3037, q_gen_3038, q_gen_3039, q_gen_3040, q_gen_3041, q_gen_3042, q_gen_3043, q_gen_3044, q_gen_3045, q_gen_3046, q_gen_3047, q_gen_3048, q_gen_3049, q_gen_3050, q_gen_3051, q_gen_3052, q_gen_3053},
Q_f={},
Delta=
{
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2951
<cons>(q_gen_2951, q_gen_2945) -> q_gen_2962
<cons>(q_gen_2946, q_gen_2945) -> q_gen_3008
<nil, nil>() -> q_gen_2929
<nil, b>() -> q_gen_2930
<b, nil>() -> q_gen_2931
<b, b>() -> q_gen_2932
<nil, a>() -> q_gen_2936
<a, nil>() -> q_gen_2937
<a, a>() -> q_gen_2938
<cons, cons>(q_gen_2938, q_gen_2937, q_gen_2936, q_gen_2929) -> q_gen_2943
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2944
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2947
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2949
<cons, b>(q_gen_2951, q_gen_2945) -> q_gen_2950
<b, cons>(q_gen_2951, q_gen_2945) -> q_gen_2952
<cons, a>(q_gen_2951, q_gen_2945) -> q_gen_2957
<a, cons>(q_gen_2951, q_gen_2945) -> q_gen_2958
<cons, cons>(q_gen_2932, q_gen_2952, q_gen_2950, q_gen_2949) -> q_gen_2960
<cons, b>(q_gen_2951, q_gen_2962) -> q_gen_2961
<b, cons>(q_gen_2951, q_gen_2962) -> q_gen_2963
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2982
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_3004
<a, b>() -> q_gen_3005
<nil, cons>(q_gen_2951, q_gen_2945) -> q_gen_3015
<b, a>() -> q_gen_3016
<nil, nil, nil>() -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2928
<nil, cons, cons>(q_gen_2938, q_gen_2937, q_gen_2936, q_gen_2929) -> q_gen_2935
<cons, nil, cons>(q_gen_2938, q_gen_2937, q_gen_2936, q_gen_2929) -> q_gen_2941
<cons, nil, cons>(q_gen_2932, q_gen_2947, q_gen_2944, q_gen_2943) -> q_gen_2942
<nil, cons, cons>(q_gen_2932, q_gen_2952, q_gen_2950, q_gen_2949) -> q_gen_2948
<cons, nil, cons>(q_gen_2938, q_gen_2958, q_gen_2957, q_gen_2949) -> q_gen_2956
<nil, cons, cons>(q_gen_2932, q_gen_2963, q_gen_2961, q_gen_2960) -> q_gen_2959
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2966
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2968) -> q_gen_2967
<nil, nil, cons>(q_gen_2951, q_gen_2945) -> q_gen_2968
<nil, nil, b>() -> q_gen_2969
<nil, b, cons>(q_gen_2951, q_gen_2945) -> q_gen_2970
<nil, b, b>() -> q_gen_2971
<b, nil, cons>(q_gen_2951, q_gen_2945) -> q_gen_2972
<b, nil, b>() -> q_gen_2973
<b, b, cons>(q_gen_2951, q_gen_2945) -> q_gen_2974
<b, b, b>() -> q_gen_2975
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2980
<cons, nil, cons>(q_gen_2932, q_gen_2947, q_gen_2930, q_gen_2982) -> q_gen_2981
<cons, cons, cons>(q_gen_2988, q_gen_2987, q_gen_2973, q_gen_2986, q_gen_2985, q_gen_2984, q_gen_2969, q_gen_2980) -> q_gen_2983
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2984
<nil, a, b>() -> q_gen_2985
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2986
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2987
<b, a, b>() -> q_gen_2988
<cons, cons, cons>(q_gen_2995, q_gen_2994, q_gen_2993, q_gen_2992, q_gen_2991, q_gen_2970, q_gen_2990, q_gen_2968) -> q_gen_2989
<nil, nil, a>() -> q_gen_2990
<nil, b, a>() -> q_gen_2991
<a, nil, cons>(q_gen_2951, q_gen_2945) -> q_gen_2992
<a, nil, a>() -> q_gen_2993
<a, b, cons>(q_gen_2951, q_gen_2945) -> q_gen_2994
<a, b, a>() -> q_gen_2995
<cons, cons, cons>(q_gen_3000, q_gen_2999, q_gen_2993, q_gen_2998, q_gen_2997, q_gen_2984, q_gen_2990, q_gen_2980) -> q_gen_2996
<nil, a, a>() -> q_gen_2997
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2998
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2999
<a, a, a>() -> q_gen_3000
<nil, cons, cons>(q_gen_2932, q_gen_2947, q_gen_2944, q_gen_2943) -> q_gen_3001
<cons, cons, cons>(q_gen_2975, q_gen_3011, q_gen_3010, q_gen_3009, q_gen_2971, q_gen_3007, q_gen_3006, q_gen_3003) -> q_gen_3002
<nil, cons, cons>(q_gen_3005, q_gen_3004, q_gen_2930, q_gen_2982) -> q_gen_3003
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_3006
<nil, b, cons>(q_gen_2951, q_gen_3008) -> q_gen_3007
<b, cons, cons>(q_gen_3005, q_gen_3004, q_gen_2930, q_gen_2982) -> q_gen_3009
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_3010
<b, b, cons>(q_gen_2951, q_gen_3008) -> q_gen_3011
<nil, cons, cons>(q_gen_2938, q_gen_2958, q_gen_2957, q_gen_2949) -> q_gen_3012
<cons, cons, cons>(q_gen_3000, q_gen_3021, q_gen_3020, q_gen_3019, q_gen_2997, q_gen_3018, q_gen_3017, q_gen_3014) -> q_gen_3013
<nil, cons, cons>(q_gen_3016, q_gen_2952, q_gen_2936, q_gen_3015) -> q_gen_3014
<nil, cons, a>(q_gen_2951, q_gen_2945) -> q_gen_3017
<nil, a, cons>(q_gen_2946, q_gen_2962) -> q_gen_3018
<a, cons, cons>(q_gen_3016, q_gen_2952, q_gen_2936, q_gen_3015) -> q_gen_3019
<a, cons, a>(q_gen_2951, q_gen_2945) -> q_gen_3020
<a, a, cons>(q_gen_2946, q_gen_2962) -> q_gen_3021
<cons, cons, cons>(q_gen_2975, q_gen_3028, q_gen_2973, q_gen_3027, q_gen_3026, q_gen_3025, q_gen_3024, q_gen_3023) -> q_gen_3022
<cons, nil, cons>(q_gen_2932, q_gen_2952, q_gen_2930, q_gen_3015) -> q_gen_3023
<cons, nil, b>(q_gen_2951, q_gen_2945) -> q_gen_3024
<cons, b, cons>(q_gen_2932, q_gen_2952, q_gen_2930, q_gen_3015) -> q_gen_3025
<cons, b, b>(q_gen_2951, q_gen_2945) -> q_gen_3026
<b, nil, cons>(q_gen_2951, q_gen_2962) -> q_gen_3027
<b, b, cons>(q_gen_2951, q_gen_2962) -> q_gen_3028
<cons, cons, cons>(q_gen_2988, q_gen_3031, q_gen_2973, q_gen_2972, q_gen_2985, q_gen_3030, q_gen_2969, q_gen_2968) -> q_gen_3029
<nil, a, cons>(q_gen_2951, q_gen_2945) -> q_gen_3030
<b, a, cons>(q_gen_2951, q_gen_2945) -> q_gen_3031
<cons, cons, cons>(q_gen_2988, q_gen_3035, q_gen_2973, q_gen_3027, q_gen_3034, q_gen_3033, q_gen_3024, q_gen_3023) -> q_gen_3032
<cons, a, cons>(q_gen_2932, q_gen_2952, q_gen_2930, q_gen_3015) -> q_gen_3033
<cons, a, b>(q_gen_2951, q_gen_2945) -> q_gen_3034
<b, a, cons>(q_gen_2951, q_gen_2962) -> q_gen_3035
<cons, cons, cons>(q_gen_2995, q_gen_3040, q_gen_2993, q_gen_3039, q_gen_3038, q_gen_3025, q_gen_3037, q_gen_3023) -> q_gen_3036
<cons, nil, a>(q_gen_2951, q_gen_2945) -> q_gen_3037
<cons, b, a>(q_gen_2951, q_gen_2945) -> q_gen_3038
<a, nil, cons>(q_gen_2951, q_gen_2962) -> q_gen_3039
<a, b, cons>(q_gen_2951, q_gen_2962) -> q_gen_3040
<cons, cons, cons>(q_gen_3000, q_gen_3043, q_gen_2993, q_gen_3039, q_gen_3042, q_gen_3033, q_gen_3037, q_gen_3023) -> q_gen_3041
<cons, a, a>(q_gen_2951, q_gen_2945) -> q_gen_3042
<a, a, cons>(q_gen_2951, q_gen_2962) -> q_gen_3043
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_3047, q_gen_3046, q_gen_2971, q_gen_2970, q_gen_3045, q_gen_2966) -> q_gen_3044
<nil, cons, b>(q_gen_2951, q_gen_2945) -> q_gen_3045
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_3046
<b, cons, b>(q_gen_2951, q_gen_2945) -> q_gen_3047
<cons, cons, cons>(q_gen_2975, q_gen_3028, q_gen_3047, q_gen_3050, q_gen_3026, q_gen_3025, q_gen_3049, q_gen_2967) -> q_gen_3048
<cons, cons, b>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_3049
<b, cons, cons>(q_gen_2932, q_gen_2952, q_gen_2930, q_gen_3015) -> q_gen_3050
<cons, cons, cons>(q_gen_2995, q_gen_3040, q_gen_3020, q_gen_3053, q_gen_3038, q_gen_3025, q_gen_3052, q_gen_2967) -> q_gen_3051
<cons, cons, a>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_3052
<a, cons, cons>(q_gen_2932, q_gen_2952, q_gen_2930, q_gen_3015) -> q_gen_3053
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923, q_gen_2927, q_gen_2933, q_gen_2934},
Q_f={},
Delta=
{
<z>() -> q_gen_2923
<s>(q_gen_2923) -> q_gen_2934
<z, s>(q_gen_2923) -> q_gen_2922
<s, s>(q_gen_2922) -> q_gen_2927
<z, s>(q_gen_2934) -> q_gen_2933
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2925, q_gen_2926, q_gen_2939, q_gen_2940, q_gen_2953, q_gen_2954, q_gen_2955, q_gen_2964, q_gen_2965, q_gen_2976, q_gen_2977, q_gen_2978, q_gen_2979},
Q_f={},
Delta=
{
<z>() -> q_gen_2955
<s>(q_gen_2955) -> q_gen_2979
<nil, z>() -> q_gen_2921
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2925
<b, z>() -> q_gen_2926
<cons, s>(q_gen_2940, q_gen_2921) -> q_gen_2939
<a, z>() -> q_gen_2940
<cons, s>(q_gen_2954, q_gen_2939) -> q_gen_2953
<b, s>(q_gen_2955) -> q_gen_2954
<cons, s>(q_gen_2965, q_gen_2925) -> q_gen_2964
<a, s>(q_gen_2955) -> q_gen_2965
<cons, s>(q_gen_2954, q_gen_2925) -> q_gen_2976
<cons, s>(q_gen_2978, q_gen_2976) -> q_gen_2977
<b, s>(q_gen_2979) -> q_gen_2978
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004422 s (model generation: 0.003922,  model checking: 0.000500):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> le([z, s(nn2)]) -> 0  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 1  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 1  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1  ;  (le([s(nn1), z])) -> BOT -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 1
}
Sat witness: Yes: (() -> length([nil, z]), {

})

-------------------------------------------
Step 1, which took 0.003512 s (model generation: 0.003471,  model checking: 0.000041):

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

}

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

}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921},
Q_f={q_gen_2921},
Delta=
{
<nil, z>() -> q_gen_2921
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 1  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 1  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1  ;  (le([s(nn1), z])) -> BOT -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 1
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.003707 s (model generation: 0.003446,  model checking: 0.000261):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<z>() -> q_gen_2923
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921},
Q_f={q_gen_2921},
Delta=
{
<nil, z>() -> q_gen_2921
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 1  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 1  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1  ;  (le([s(nn1), z])) -> BOT -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 1
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.003999 s (model generation: 0.003449,  model checking: 0.000550):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<z>() -> q_gen_2923
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921},
Q_f={q_gen_2921},
Delta=
{
<nil, z>() -> q_gen_2921
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 1  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 1  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 1  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 1  ;  (le([s(nn1), z])) -> BOT -> 1  ;  (le([z, z])) -> BOT -> 1  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 4
}
Sat witness: Yes: ((length([ll, _es])) -> length([cons(x, ll), s(_es)]), {
_es -> z  ;  ll -> nil  ;  x -> b
})

-------------------------------------------
Step 4, which took 0.003511 s (model generation: 0.003434,  model checking: 0.000077):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<z>() -> q_gen_2923
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 1  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 1  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2  ;  (le([s(nn1), z])) -> BOT -> 2  ;  (le([z, z])) -> BOT -> 2  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 4
}
Sat witness: Yes: ((le([nn1, nn2])) -> le([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> s(z)
})

-------------------------------------------
Step 5, which took 0.005435 s (model generation: 0.004347,  model checking: 0.001088):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> le([z, s(nn2)]) -> 3  ;  () -> length([nil, z]) -> 3  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 1  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 4  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 2  ;  (le([s(nn1), z])) -> BOT -> 2  ;  (le([z, z])) -> BOT -> 2  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 4
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 6, which took 0.006277 s (model generation: 0.006050,  model checking: 0.000227):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932},
Q_f={q_gen_2924},
Delta=
{
<nil, nil>() -> q_gen_2929
<nil, b>() -> q_gen_2930
<b, nil>() -> q_gen_2931
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 2  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 4  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 3  ;  (le([s(nn1), z])) -> BOT -> 3  ;  (le([z, z])) -> BOT -> 3  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 4
}
Sat witness: Yes: (() -> le([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 7, which took 0.010430 s (model generation: 0.008970,  model checking: 0.001460):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932},
Q_f={q_gen_2924},
Delta=
{
<nil, nil>() -> q_gen_2929
<nil, b>() -> q_gen_2930
<b, nil>() -> q_gen_2931
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 3  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 4  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4  ;  (le([s(nn1), z])) -> BOT -> 4  ;  (le([z, z])) -> BOT -> 4  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 4
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 8, which took 0.009330 s (model generation: 0.008840,  model checking: 0.000490):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932},
Q_f={q_gen_2924},
Delta=
{
<nil, nil>() -> q_gen_2929
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, nil>() -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 4  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 4  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 4  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 4  ;  (le([s(nn1), z])) -> BOT -> 4  ;  (le([z, z])) -> BOT -> 4  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 7
}
Sat witness: Yes: ((length([ll, _es])) -> length([cons(x, ll), s(_es)]), {
_es -> z  ;  ll -> nil  ;  x -> a
})

-------------------------------------------
Step 9, which took 0.020183 s (model generation: 0.012812,  model checking: 0.007371):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932},
Q_f={q_gen_2924},
Delta=
{
<nil, nil>() -> q_gen_2929
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, nil>() -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, z>() -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6  ;  () -> le([z, s(nn2)]) -> 6  ;  () -> length([nil, z]) -> 4  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 4  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 7  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 5  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 5  ;  (le([s(nn1), z])) -> BOT -> 5  ;  (le([z, z])) -> BOT -> 5  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 7
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 10, which took 0.019376 s (model generation: 0.006219,  model checking: 0.013157):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946},
Q_f={q_gen_2924},
Delta=
{
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, z>() -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> le([z, s(nn2)]) -> 7  ;  () -> length([nil, z]) -> 5  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 5  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 7  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 6  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 6  ;  (le([s(nn1), z])) -> BOT -> 6  ;  (le([z, z])) -> BOT -> 6  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 7
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 11, which took 0.005875 s (model generation: 0.005597,  model checking: 0.000278):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946},
Q_f={q_gen_2924},
Delta=
{
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926},
Q_f={q_gen_2921},
Delta=
{
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, z>() -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> le([z, s(nn2)]) -> 7  ;  () -> length([nil, z]) -> 6  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 6  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 7  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 7  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 7  ;  (le([s(nn1), z])) -> BOT -> 7  ;  (le([z, z])) -> BOT -> 7  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 10
}
Sat witness: Yes: ((length([ll, _es])) -> length([cons(x, ll), s(_es)]), {
_es -> s(z)  ;  ll -> cons(a, nil)  ;  x -> b
})

-------------------------------------------
Step 12, which took 0.011466 s (model generation: 0.005655,  model checking: 0.005811):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946},
Q_f={q_gen_2924},
Delta=
{
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9  ;  () -> le([z, s(nn2)]) -> 7  ;  () -> length([nil, z]) -> 7  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 7  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 8  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 8  ;  (le([s(nn1), z])) -> BOT -> 8  ;  (le([z, z])) -> BOT -> 8  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 10
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, nil)  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 13, which took 0.013888 s (model generation: 0.005770,  model checking: 0.008118):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946},
Q_f={q_gen_2924},
Delta=
{
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> le([z, s(nn2)]) -> 8  ;  () -> length([nil, z]) -> 8  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 8  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 9  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 9  ;  (le([s(nn1), z])) -> BOT -> 9  ;  (le([z, z])) -> BOT -> 9  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 10
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(b, cons(b, cons(b, nil)))
})

-------------------------------------------
Step 14, which took 0.006605 s (model generation: 0.006251,  model checking: 0.000354):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> le([z, s(nn2)]) -> 9  ;  () -> length([nil, z]) -> 9  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 9  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 10  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 10  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 10  ;  (le([s(nn1), z])) -> BOT -> 10  ;  (le([z, z])) -> BOT -> 10  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 13
}
Sat witness: Yes: ((length([ll, _es])) -> length([cons(x, ll), s(_es)]), {
_es -> s(z)  ;  ll -> cons(b, nil)  ;  x -> a
})

-------------------------------------------
Step 15, which took 0.012379 s (model generation: 0.007671,  model checking: 0.004708):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12  ;  () -> le([z, s(nn2)]) -> 10  ;  () -> length([nil, z]) -> 10  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 10  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 13  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 11  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 11  ;  (le([s(nn1), z])) -> BOT -> 11  ;  (le([z, z])) -> BOT -> 11  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 13
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.016768 s (model generation: 0.010822,  model checking: 0.005946):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, nil, b>() -> q_gen_2969
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, b>() -> q_gen_2971
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, nil, b>() -> q_gen_2973
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> le([z, s(nn2)]) -> 11  ;  () -> length([nil, z]) -> 11  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 11  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 13  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 12  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 12  ;  (le([s(nn1), z])) -> BOT -> 12  ;  (le([z, z])) -> BOT -> 12  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 16
}
Sat witness: Yes: ((length([ll, _es])) -> length([cons(x, ll), s(_es)]), {
_es -> s(s(z))  ;  ll -> cons(b, cons(b, nil))  ;  x -> b
})

-------------------------------------------
Step 17, which took 0.048328 s (model generation: 0.015779,  model checking: 0.032549):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, nil, b>() -> q_gen_2969
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, b>() -> q_gen_2971
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, nil, b>() -> q_gen_2973
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13  ;  () -> le([z, s(nn2)]) -> 12  ;  () -> length([nil, z]) -> 12  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 12  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 16  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 13  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 13  ;  (le([s(nn1), z])) -> BOT -> 13  ;  (le([z, z])) -> BOT -> 13  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 16
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.071977 s (model generation: 0.009330,  model checking: 0.062647):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, nil, b>() -> q_gen_2969
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, b>() -> q_gen_2971
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, nil, b>() -> q_gen_2973
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14  ;  () -> le([z, s(nn2)]) -> 13  ;  () -> length([nil, z]) -> 13  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 13  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 19  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 14  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 14  ;  (le([s(nn1), z])) -> BOT -> 14  ;  (le([z, z])) -> BOT -> 14  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 17
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.211768 s (model generation: 0.010062,  model checking: 0.201706):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, nil, b>() -> q_gen_2969
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, a, b>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, nil, b>() -> q_gen_2973
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15  ;  () -> le([z, s(nn2)]) -> 14  ;  () -> length([nil, z]) -> 14  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 14  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 22  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 15  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 15  ;  (le([s(nn1), z])) -> BOT -> 15  ;  (le([z, z])) -> BOT -> 15  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 18
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 20, which took 0.072153 s (model generation: 0.011628,  model checking: 0.060525):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, nil, a>() -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16  ;  () -> le([z, s(nn2)]) -> 15  ;  () -> length([nil, z]) -> 15  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 15  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 25  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 16  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 16  ;  (le([s(nn1), z])) -> BOT -> 16  ;  (le([z, z])) -> BOT -> 16  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 19
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 1.049999 s (model generation: 0.011894,  model checking: 1.038105):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, nil, a>() -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17  ;  () -> le([z, s(nn2)]) -> 16  ;  () -> length([nil, z]) -> 16  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 16  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 28  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 17  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 17  ;  (le([s(nn1), z])) -> BOT -> 17  ;  (le([z, z])) -> BOT -> 17  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 20
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 22, which took 0.555752 s (model generation: 0.014474,  model checking: 0.541278):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18  ;  () -> le([z, s(nn2)]) -> 17  ;  () -> length([nil, z]) -> 17  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 17  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 31  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 18  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 18  ;  (le([s(nn1), z])) -> BOT -> 18  ;  (le([z, z])) -> BOT -> 18  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 21
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 3.199597 s (model generation: 0.019094,  model checking: 3.180503):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<nil, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2973
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19  ;  () -> le([z, s(nn2)]) -> 18  ;  () -> length([nil, z]) -> 18  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 18  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 34  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 19  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 19  ;  (le([s(nn1), z])) -> BOT -> 19  ;  (le([z, z])) -> BOT -> 19  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 22
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 1.476374 s (model generation: 0.021292,  model checking: 1.455082):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<cons, nil, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<cons, b, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<cons, b, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2973
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20  ;  () -> le([z, s(nn2)]) -> 19  ;  () -> length([nil, z]) -> 19  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 19  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 37  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 20  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 20  ;  (le([s(nn1), z])) -> BOT -> 20  ;  (le([z, z])) -> BOT -> 20  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 23
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 25, which took 2.990281 s (model generation: 0.024537,  model checking: 2.965744):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<cons, nil, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<cons, a, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<cons, b, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<cons, a, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2973
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21  ;  () -> le([z, s(nn2)]) -> 20  ;  () -> length([nil, z]) -> 20  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 20  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 40  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 21  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 21  ;  (le([s(nn1), z])) -> BOT -> 21  ;  (le([z, z])) -> BOT -> 21  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 24
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 26, which took 3.010549 s (model generation: 0.032319,  model checking: 2.978230):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<cons, nil, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<cons, nil, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<cons, a, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<cons, b, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<cons, a, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, a>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2973
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22  ;  () -> le([z, s(nn2)]) -> 21  ;  () -> length([nil, z]) -> 21  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 21  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 43  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 22  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 22  ;  (le([s(nn1), z])) -> BOT -> 22  ;  (le([z, z])) -> BOT -> 22  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 25
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 27, which took 1.571725 s (model generation: 0.037523,  model checking: 1.534202):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<cons, nil, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<cons, nil, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<cons, a, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<cons, b, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<cons, a, a>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, a, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, a>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2973
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23  ;  () -> le([z, s(nn2)]) -> 22  ;  () -> length([nil, z]) -> 22  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 22  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 46  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 23  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 23  ;  (le([s(nn1), z])) -> BOT -> 23  ;  (le([z, z])) -> BOT -> 23  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 26
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 7.002704 s (model generation: 0.043837,  model checking: 6.958867):

Model:
|_
{
append -> 
{{{
Q={q_gen_2924, q_gen_2929, q_gen_2930, q_gen_2931, q_gen_2932, q_gen_2945, q_gen_2946, q_gen_2969, q_gen_2970, q_gen_2971, q_gen_2972, q_gen_2973, q_gen_2974, q_gen_2975},
Q_f={q_gen_2924},
Delta=
{
<cons>(q_gen_2946, q_gen_2945) -> q_gen_2945
<nil>() -> q_gen_2945
<a>() -> q_gen_2946
<b>() -> q_gen_2946
<cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2929
<nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2929
<nil, nil>() -> q_gen_2929
<cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2930
<cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2930
<nil, a>() -> q_gen_2930
<nil, b>() -> q_gen_2930
<a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<a, nil>() -> q_gen_2931
<b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2931
<b, nil>() -> q_gen_2931
<a, a>() -> q_gen_2932
<a, b>() -> q_gen_2932
<b, a>() -> q_gen_2932
<b, b>() -> q_gen_2932
<cons, cons, cons>(q_gen_2975, q_gen_2974, q_gen_2973, q_gen_2972, q_gen_2971, q_gen_2970, q_gen_2969, q_gen_2924) -> q_gen_2924
<cons, nil, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2924
<nil, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2924
<nil, nil, nil>() -> q_gen_2924
<cons, cons, b>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2969
<cons, nil, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<cons, nil, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2969
<nil, nil, a>() -> q_gen_2969
<nil, nil, b>() -> q_gen_2969
<cons, a, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<cons, b, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2970
<nil, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<nil, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2970
<cons, a, a>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, a, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, a>(q_gen_2946, q_gen_2945) -> q_gen_2971
<cons, b, b>(q_gen_2946, q_gen_2945) -> q_gen_2971
<nil, a, a>() -> q_gen_2971
<nil, a, b>() -> q_gen_2971
<nil, b, a>() -> q_gen_2971
<nil, b, b>() -> q_gen_2971
<a, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<a, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<b, cons, cons>(q_gen_2932, q_gen_2931, q_gen_2930, q_gen_2929) -> q_gen_2972
<b, nil, cons>(q_gen_2946, q_gen_2945) -> q_gen_2972
<a, cons, a>(q_gen_2946, q_gen_2945) -> q_gen_2973
<a, nil, a>() -> q_gen_2973
<b, cons, b>(q_gen_2946, q_gen_2945) -> q_gen_2973
<b, nil, b>() -> q_gen_2973
<a, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, a, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<b, b, cons>(q_gen_2946, q_gen_2945) -> q_gen_2974
<a, a, a>() -> q_gen_2975
<a, b, a>() -> q_gen_2975
<b, a, b>() -> q_gen_2975
<b, b, b>() -> q_gen_2975
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: complete
}}}
  ;  le -> 
{{{
Q={q_gen_2922, q_gen_2923},
Q_f={q_gen_2922},
Delta=
{
<s>(q_gen_2923) -> q_gen_2923
<z>() -> q_gen_2923
<s, s>(q_gen_2922) -> q_gen_2922
<z, s>(q_gen_2923) -> q_gen_2922
}

Datatype: <nat, nat>
Convolution form: complete
}}}
  ;  length -> 
{{{
Q={q_gen_2921, q_gen_2926, q_gen_2955},
Q_f={q_gen_2921},
Delta=
{
<s>(q_gen_2955) -> q_gen_2955
<z>() -> q_gen_2955
<cons, s>(q_gen_2926, q_gen_2921) -> q_gen_2921
<nil, z>() -> q_gen_2921
<a, s>(q_gen_2955) -> q_gen_2926
<a, z>() -> q_gen_2926
<b, s>(q_gen_2955) -> q_gen_2926
<b, z>() -> q_gen_2926
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> le([z, s(nn2)]) -> 23  ;  () -> length([nil, z]) -> 23  ;  (append([l1, l2, _os]) /\ le([z, _ns]) /\ length([_os, _ps]) /\ length([l1, _ns])) -> le([z, _ps]) -> 23  ;  (append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]) -> 49  ;  (le([nn1, nn2])) -> le([s(nn1), s(nn2)]) -> 24  ;  (le([s(nn1), s(nn2)])) -> le([nn1, nn2]) -> 24  ;  (le([s(nn1), z])) -> BOT -> 24  ;  (le([z, z])) -> BOT -> 24  ;  (length([ll, _es])) -> length([cons(x, ll), s(_es)]) -> 27
}
Sat witness: Yes: ((append([t1, l2, _is])) -> append([cons(h1, t1), l2, cons(h1, _is)]), {
_is -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(b, nil)
})

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