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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)])}
(append([_kaa, _laa, _maa]) /\ append([_kaa, _laa, _naa])) -> eq_natlist([_maa, _naa])
)
}

properties:
{(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 0
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 0
}


Solving took 60.182554 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7033, q_gen_7034, q_gen_7035, q_gen_7036, q_gen_7037, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7042, q_gen_7043, q_gen_7044, q_gen_7045, q_gen_7046, q_gen_7047, q_gen_7048, q_gen_7049, q_gen_7050, q_gen_7051, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7055, q_gen_7056, q_gen_7057, q_gen_7058, q_gen_7059, q_gen_7060, q_gen_7061, q_gen_7062, q_gen_7063, q_gen_7064, q_gen_7065, q_gen_7066, q_gen_7067, q_gen_7068, q_gen_7069, q_gen_7070, q_gen_7071, q_gen_7072, q_gen_7073, q_gen_7074, q_gen_7075, q_gen_7076, q_gen_7077, q_gen_7078, q_gen_7079, q_gen_7080, q_gen_7081, q_gen_7082, q_gen_7083, q_gen_7084, q_gen_7085, q_gen_7086, q_gen_7087, q_gen_7088, q_gen_7089, q_gen_7090, q_gen_7091, q_gen_7092, q_gen_7093, q_gen_7094, q_gen_7095, q_gen_7096, q_gen_7097, q_gen_7098, q_gen_7099, q_gen_7100, q_gen_7101, q_gen_7102, q_gen_7103, q_gen_7104, q_gen_7105, q_gen_7106, q_gen_7107, q_gen_7108, q_gen_7109, q_gen_7110, q_gen_7111, q_gen_7112, q_gen_7113, q_gen_7114, q_gen_7115, q_gen_7116, q_gen_7117, q_gen_7118, q_gen_7119, q_gen_7120, q_gen_7121, q_gen_7122, q_gen_7123, q_gen_7124, q_gen_7125, q_gen_7126, q_gen_7127, q_gen_7128, q_gen_7129, q_gen_7130, q_gen_7131, q_gen_7132, q_gen_7133, q_gen_7134, q_gen_7135, q_gen_7136, q_gen_7137, q_gen_7138, q_gen_7139, q_gen_7140, q_gen_7141, q_gen_7142, q_gen_7143, q_gen_7144, q_gen_7145, q_gen_7146},
Q_f={},
Delta=
{
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7047
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7073
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7034
<s, s>(q_gen_7032) -> q_gen_7035
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7061
<cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7065
<s, s>(q_gen_7035) -> q_gen_7066
<cons, cons>(q_gen_7032, q_gen_7061) -> q_gen_7115
<cons, cons>(q_gen_7035, q_gen_7061) -> q_gen_7117
<nil, cons>(q_gen_7040, q_gen_7047) -> q_gen_7131
<cons, cons>(q_gen_7136, q_gen_7031) -> q_gen_7135
<s, s>(q_gen_7066) -> q_gen_7136
<nil, nil, nil>() -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, cons, cons>(q_gen_7035, q_gen_7034) -> q_gen_7033
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7036
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7037
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<z, z, z>() -> q_gen_7041
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7042
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7044
<cons, cons, cons>(q_gen_7041, q_gen_7046) -> q_gen_7045
<nil, nil, cons>(q_gen_7040, q_gen_7047) -> q_gen_7046
<cons, cons, cons>(q_gen_7049, q_gen_7046) -> q_gen_7048
<s, z, s>(q_gen_7032) -> q_gen_7049
<nil, cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7050
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7051
<nil, nil, cons>(q_gen_7053, q_gen_7047) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7049, q_gen_7029) -> q_gen_7056
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7057
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7058
<cons, cons, cons>(q_gen_7049, q_gen_7038) -> q_gen_7059
<nil, cons, cons>(q_gen_7032, q_gen_7061) -> q_gen_7060
<cons, cons, cons>(q_gen_7054, q_gen_7036) -> q_gen_7062
<cons, cons, cons>(q_gen_7049, q_gen_7036) -> q_gen_7063
<nil, cons, cons>(q_gen_7066, q_gen_7065) -> q_gen_7064
<cons, cons, cons>(q_gen_7054, q_gen_7068) -> q_gen_7067
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7068
<cons, cons, cons>(q_gen_7049, q_gen_7068) -> q_gen_7069
<nil, cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7070
<cons, cons, cons>(q_gen_7074, q_gen_7072) -> q_gen_7071
<nil, nil, cons>(q_gen_7073, q_gen_7039) -> q_gen_7072
<s, s, s>(q_gen_7075) -> q_gen_7074
<z, s, z>(q_gen_7040) -> q_gen_7075
<cons, nil, cons>(q_gen_7066, q_gen_7031) -> q_gen_7076
<cons, cons, cons>(q_gen_7078, q_gen_7030) -> q_gen_7077
<z, s, z>(q_gen_7053) -> q_gen_7078
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7079
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7080
<cons, cons, cons>(q_gen_7078, q_gen_7057) -> q_gen_7081
<cons, cons, cons>(q_gen_7049, q_gen_7083) -> q_gen_7082
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7083
<cons, cons, cons>(q_gen_7075, q_gen_7085) -> q_gen_7084
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7085
<cons, cons, cons>(q_gen_7041, q_gen_7085) -> q_gen_7086
<cons, cons, cons>(q_gen_7041, q_gen_7083) -> q_gen_7087
<cons, nil, cons>(q_gen_7035, q_gen_7061) -> q_gen_7088
<cons, cons, cons>(q_gen_7074, q_gen_7038) -> q_gen_7089
<cons, cons, cons>(q_gen_7078, q_gen_7029) -> q_gen_7090
<cons, cons, cons>(q_gen_7075, q_gen_7036) -> q_gen_7091
<cons, cons, cons>(q_gen_7075, q_gen_7029) -> q_gen_7092
<cons, cons, cons>(q_gen_7054, q_gen_7030) -> q_gen_7093
<cons, cons, cons>(q_gen_7095, q_gen_7029) -> q_gen_7094
<s, z, s>(q_gen_7035) -> q_gen_7095
<cons, cons, cons>(q_gen_7078, q_gen_7083) -> q_gen_7096
<cons, cons, cons>(q_gen_7075, q_gen_7083) -> q_gen_7097
<cons, cons, cons>(q_gen_7075, q_gen_7057) -> q_gen_7098
<cons, cons, cons>(q_gen_7100, q_gen_7029) -> q_gen_7099
<s, s, s>(q_gen_7095) -> q_gen_7100
<cons, cons, cons>(q_gen_7102, q_gen_7029) -> q_gen_7101
<s, s, s>(q_gen_7049) -> q_gen_7102
<cons, cons, cons>(q_gen_7104, q_gen_7029) -> q_gen_7103
<s, s, s>(q_gen_7078) -> q_gen_7104
<cons, cons, cons>(q_gen_7075, q_gen_7030) -> q_gen_7105
<cons, cons, cons>(q_gen_7054, q_gen_7107) -> q_gen_7106
<cons, nil, cons>(q_gen_7032, q_gen_7061) -> q_gen_7107
<cons, cons, cons>(q_gen_7075, q_gen_7109) -> q_gen_7108
<cons, cons, cons>(q_gen_7041, q_gen_7068) -> q_gen_7109
<cons, cons, cons>(q_gen_7041, q_gen_7079) -> q_gen_7110
<cons, cons, cons>(q_gen_7074, q_gen_7083) -> q_gen_7111
<cons, cons, cons>(q_gen_7054, q_gen_7083) -> q_gen_7112
<nil, cons, cons>(q_gen_7035, q_gen_7061) -> q_gen_7113
<nil, cons, cons>(q_gen_7032, q_gen_7115) -> q_gen_7114
<nil, cons, cons>(q_gen_7032, q_gen_7117) -> q_gen_7116
<cons, cons, cons>(q_gen_7095, q_gen_7038) -> q_gen_7118
<cons, cons, cons>(q_gen_7041, q_gen_7120) -> q_gen_7119
<cons, nil, cons>(q_gen_7066, q_gen_7043) -> q_gen_7120
<cons, cons, cons>(q_gen_7075, q_gen_7044) -> q_gen_7121
<cons, cons, cons>(q_gen_7041, q_gen_7044) -> q_gen_7122
<cons, cons, cons>(q_gen_7125, q_gen_7124) -> q_gen_7123
<cons, cons, cons>(q_gen_7041, q_gen_7036) -> q_gen_7124
<s, s, s>(q_gen_7102) -> q_gen_7125
<cons, cons, cons>(q_gen_7100, q_gen_7124) -> q_gen_7126
<cons, cons, cons>(q_gen_7128, q_gen_7044) -> q_gen_7127
<s, s, s>(q_gen_7054) -> q_gen_7128
<cons, cons, cons>(q_gen_7074, q_gen_7044) -> q_gen_7129
<cons, nil, cons>(q_gen_7035, q_gen_7131) -> q_gen_7130
<cons, cons, cons>(q_gen_7075, q_gen_7122) -> q_gen_7132
<cons, cons, cons>(q_gen_7041, q_gen_7045) -> q_gen_7133
<nil, cons, cons>(q_gen_7136, q_gen_7135) -> q_gen_7134
<cons, cons, cons>(q_gen_7075, q_gen_7138) -> q_gen_7137
<cons, cons, cons>(q_gen_7041, q_gen_7139) -> q_gen_7138
<cons, cons, cons>(q_gen_7078, q_gen_7085) -> q_gen_7139
<cons, cons, cons>(q_gen_7075, q_gen_7141) -> q_gen_7140
<cons, cons, cons>(q_gen_7041, q_gen_7142) -> q_gen_7141
<cons, cons, cons>(q_gen_7078, q_gen_7097) -> q_gen_7142
<cons, cons, cons>(q_gen_7078, q_gen_7038) -> q_gen_7143
<cons, cons, cons>(q_gen_7145, q_gen_7029) -> q_gen_7144
<s, z, s>(q_gen_7066) -> q_gen_7145
<cons, cons, cons>(q_gen_7104, q_gen_7083) -> q_gen_7146
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008748 s (model generation: 0.008445,  model checking: 0.000303):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 1
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 1, which took 0.008845 s (model generation: 0.007724,  model checking: 0.001121):

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

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 1
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.010889 s (model generation: 0.010448,  model checking: 0.000441):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032},
Q_f={q_gen_7029},
Delta=
{
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 2
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 3, which took 0.011791 s (model generation: 0.009482,  model checking: 0.002309):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032},
Q_f={q_gen_7029},
Delta=
{
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 3
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.012721 s (model generation: 0.009773,  model checking: 0.002948):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 4
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 10
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.015707 s (model generation: 0.010916,  model checking: 0.004791):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 5
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 6, which took 0.017744 s (model generation: 0.011427,  model checking: 0.006317):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 6
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 16
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.018758 s (model generation: 0.011147,  model checking: 0.007611):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 7
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.015277 s (model generation: 0.013482,  model checking: 0.001795):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 10
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), nil)  ;  _qaa -> cons(z, nil)  ;  _raa -> cons(s(z), nil)  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(s(z), nil)  ;  l2 -> nil
})

-------------------------------------------
Step 9, which took 0.019910 s (model generation: 0.018006,  model checking: 0.001904):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), nil)  ;  _qaa -> cons(z, nil)  ;  _raa -> cons(s(z), cons(z, nil))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(s(z), nil)  ;  l2 -> nil
})

-------------------------------------------
Step 10, which took 0.023654 s (model generation: 0.022881,  model checking: 0.000773):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7057},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7057
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 13
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 11, which took 0.035313 s (model generation: 0.021073,  model checking: 0.014240):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), cons(z, nil))  ;  _qaa -> cons(z, cons(z, nil))  ;  _raa -> cons(s(z), cons(z, nil))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(s(z), nil)  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 12, which took 0.027197 s (model generation: 0.026482,  model checking: 0.000715):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 16
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(s(z)), cons(s(s(z)), nil))
})

-------------------------------------------
Step 13, which took 0.032249 s (model generation: 0.028729,  model checking: 0.003520):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7035) -> q_gen_7032
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), cons(z, nil))  ;  _qaa -> cons(z, cons(z, nil))  ;  _raa -> cons(s(z), cons(z, nil))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(s(z), cons(z, nil))  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 14, which took 0.034942 s (model generation: 0.034312,  model checking: 0.000630):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7034, q_gen_7036, q_gen_7039, q_gen_7040, q_gen_7041},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7034
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7034) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7036
<cons, cons, cons>(q_gen_7041, q_gen_7036) -> q_gen_7036
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7036
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7036
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 19
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

-------------------------------------------
Step 15, which took 0.053603 s (model generation: 0.038708,  model checking: 0.014895):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 19
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 22
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(s(z)), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.049203 s (model generation: 0.047851,  model checking: 0.001352):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7055},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7035) -> q_gen_7032
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 22
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 22
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(s(z)), nil)  ;  _qaa -> cons(z, nil)  ;  _raa -> cons(z, cons(z, nil))  ;  i -> s(s(z))  ;  j -> z  ;  l1 -> cons(z, cons(z, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 17, which took 0.064151 s (model generation: 0.061265,  model checking: 0.002886):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7053) -> q_gen_7040
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, s, s>(q_gen_7054) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 22
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 25
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(z), nil)  ;  h1 -> z  ;  l2 -> cons(s(s(z)), nil)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 18, which took 0.077699 s (model generation: 0.072316,  model checking: 0.005383):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7055},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 25
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), cons(s(z), nil))  ;  _qaa -> cons(z, cons(s(z), nil))  ;  _raa -> cons(z, cons(s(z), nil))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(z, nil)  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 19, which took 0.097482 s (model generation: 0.096544,  model checking: 0.000938):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7055},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 25
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 28
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 20, which took 0.113636 s (model generation: 0.104561,  model checking: 0.009075):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7054) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 28
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 28
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), cons(z, nil))  ;  _qaa -> cons(z, nil)  ;  _raa -> cons(z, cons(z, nil))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(z, nil)  ;  l2 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 21, which took 0.135060 s (model generation: 0.133749,  model checking: 0.001311):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 28
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 31
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 22, which took 0.152438 s (model generation: 0.148476,  model checking: 0.003962):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7054) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 31
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 31
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(s(z)), nil)  ;  _qaa -> cons(z, nil)  ;  _raa -> cons(s(z), cons(z, nil))  ;  i -> s(s(z))  ;  j -> z  ;  l1 -> cons(s(z), nil)  ;  l2 -> nil
})

-------------------------------------------
Step 23, which took 0.160355 s (model generation: 0.157001,  model checking: 0.003354):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7049},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7049, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7049, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7049) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7049
<s, z, s>(q_gen_7032) -> q_gen_7049
<z, s, z>(q_gen_7040) -> q_gen_7049
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 31
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 34
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.198103 s (model generation: 0.184378,  model checking: 0.013725):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 34
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 34
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), nil)  ;  _qaa -> cons(s(s(z)), nil)  ;  _raa -> cons(z, cons(s(z), nil))  ;  i -> s(z)  ;  j -> s(s(z))  ;  l1 -> cons(z, nil)  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 25, which took 0.186628 s (model generation: 0.185214,  model checking: 0.001414):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 34
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 37
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(z), nil)  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 26, which took 0.190402 s (model generation: 0.177707,  model checking: 0.012695):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 37
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 37
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(s(z)), nil)  ;  _qaa -> cons(s(s(s(z))), nil)  ;  _raa -> cons(s(z), nil)  ;  i -> s(s(z))  ;  j -> s(s(s(z)))  ;  l1 -> cons(s(z), nil)  ;  l2 -> cons(s(z), nil)
})

-------------------------------------------
Step 27, which took 0.291157 s (model generation: 0.285702,  model checking: 0.005455):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, s, s>(q_gen_7054) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7030) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 37
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 40
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 28, which took 0.348561 s (model generation: 0.326543,  model checking: 0.022018):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7030) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 40
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 40
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(z, cons(z, nil))  ;  _qaa -> cons(s(z), cons(z, cons(z, nil)))  ;  _raa -> cons(z, cons(z, cons(z, nil)))  ;  i -> z  ;  j -> s(z)  ;  l1 -> cons(z, cons(z, cons(z, nil)))  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 29, which took 0.417039 s (model generation: 0.415774,  model checking: 0.001265):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7053, q_gen_7054},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7030
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7030
<cons, cons, cons>(q_gen_7054, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7030
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7053) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 40
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 30, which took 0.413130 s (model generation: 0.377124,  model checking: 0.036006):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7075},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7075, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7075, q_gen_7052) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7075) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7075
<z, s, z>(q_gen_7053) -> q_gen_7075
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 43
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), nil)  ;  _qaa -> cons(s(s(z)), nil)  ;  _raa -> cons(s(z), cons(s(z), nil))  ;  i -> s(z)  ;  j -> s(s(z))  ;  l1 -> cons(s(z), nil)  ;  l2 -> nil
})

-------------------------------------------
Step 31, which took 0.427324 s (model generation: 0.426912,  model checking: 0.000412):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7042, q_gen_7043},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7043
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7042) -> q_gen_7038
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7038
<nil, cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7042
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7042
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 43
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 32, which took 0.487753 s (model generation: 0.487416,  model checking: 0.000337):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7034, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7042},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7034
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7034
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7034
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7034) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7034) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7034) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7042) -> q_gen_7038
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7042
<cons, nil, cons>(q_gen_7032, q_gen_7034) -> q_gen_7042
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7042
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 43
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), nil)
})

-------------------------------------------
Step 33, which took 0.575770 s (model generation: 0.575271,  model checking: 0.000499):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7034, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7055},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7034
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7034
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, nil, cons>(q_gen_7035, q_gen_7034) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7034) -> q_gen_7030
<nil, cons, cons>(q_gen_7032, q_gen_7034) -> q_gen_7030
<nil, cons, cons>(q_gen_7035, q_gen_7034) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 43
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 34, which took 0.435452 s (model generation: 0.434882,  model checking: 0.000570):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7037, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7055, q_gen_7061},
Q_f={q_gen_7029, q_gen_7037},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7061
<cons, cons>(q_gen_7032, q_gen_7061) -> q_gen_7061
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7061) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7061) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7061) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7061) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7037) -> q_gen_7037
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7037
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 45
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 43
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 43
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(s(z), cons(z, nil)))
})

-------------------------------------------
Step 35, which took 0.558273 s (model generation: 0.553794,  model checking: 0.004479):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7030, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7055},
Q_f={q_gen_7029, q_gen_7030},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7043
<cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7043
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, nil, cons>(q_gen_7035, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7030) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7030
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7030
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7030
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 45
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 43
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 46
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(s(z)), cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 36, which took 0.513442 s (model generation: 0.501696,  model checking: 0.011746):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7033, q_gen_7034, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7055},
Q_f={q_gen_7029, q_gen_7033},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7034) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7034
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7034
<cons, cons>(q_gen_7035, q_gen_7034) -> q_gen_7034
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7034
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7033) -> q_gen_7033
<cons, nil, cons>(q_gen_7032, q_gen_7034) -> q_gen_7033
<cons, nil, cons>(q_gen_7035, q_gen_7034) -> q_gen_7033
<nil, cons, cons>(q_gen_7032, q_gen_7034) -> q_gen_7033
<nil, cons, cons>(q_gen_7035, q_gen_7034) -> q_gen_7033
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7033
<s, s, s>(q_gen_7041) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, s, z>(q_gen_7040) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7055
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 45
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 46
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 46
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(z, cons(z, nil))  ;  _qaa -> cons(s(z), cons(z, nil))  ;  _raa -> cons(z, cons(z, cons(z, nil)))  ;  i -> z  ;  j -> s(z)  ;  l1 -> cons(z, nil)  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 37, which took 0.736107 s (model generation: 0.735061,  model checking: 0.001046):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7054},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7035
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7043
<cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7043
<cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7043
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<s, z, s>(q_gen_7035) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 46
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 46
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 49
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> nil  ;  h1 -> s(z)  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 38, which took 0.951559 s (model generation: 0.617142,  model checking: 0.334417):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7054, q_gen_7066},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7043
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<s, s>(q_gen_7035) -> q_gen_7066
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7066, q_gen_7043) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<cons, nil, cons>(q_gen_7066, q_gen_7031) -> q_gen_7038
<cons, nil, cons>(q_gen_7066, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<s, z, s>(q_gen_7035) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 49
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 47
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 49
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 39, which took 0.604870 s (model generation: 0.539346,  model checking: 0.065524):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7054, q_gen_7066},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<s>(q_gen_7040) -> q_gen_7040
<z>() -> q_gen_7040
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7043
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<s, s>(q_gen_7035) -> q_gen_7066
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7066, q_gen_7043) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<cons, nil, cons>(q_gen_7066, q_gen_7031) -> q_gen_7038
<cons, nil, cons>(q_gen_7066, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7035, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7054) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, z, s>(q_gen_7035) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 49
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 50
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 49
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(s(z)), cons(z, cons(z, nil)))  ;  _qaa -> cons(s(z), cons(z, cons(z, nil)))  ;  _raa -> cons(s(s(s(z))), cons(z, cons(z, nil)))  ;  i -> s(s(z))  ;  j -> s(z)  ;  l1 -> cons(s(s(s(z))), cons(z, nil))  ;  l2 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 40, which took 0.745457 s (model generation: 0.740118,  model checking: 0.005339):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7046, q_gen_7047, q_gen_7053, q_gen_7054, q_gen_7073},
Q_f={q_gen_7029},
Delta=
{
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7047
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7073
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7046) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7046) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7046
<nil, nil, cons>(q_gen_7040, q_gen_7047) -> q_gen_7046
<nil, nil, cons>(q_gen_7053, q_gen_7047) -> q_gen_7046
<nil, nil, cons>(q_gen_7073, q_gen_7039) -> q_gen_7046
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 49
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 50
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 52
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(z), nil)  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 41, which took 1.312095 s (model generation: 1.269957,  model checking: 0.042138):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7044, q_gen_7053, q_gen_7054, q_gen_7074},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7074, q_gen_7044) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7044) -> q_gen_7044
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7044
<cons, cons, cons>(q_gen_7054, q_gen_7044) -> q_gen_7044
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7044
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7044
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7044
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
<s, s, s>(q_gen_7074) -> q_gen_7074
<z, s, z>(q_gen_7040) -> q_gen_7074
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 50
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 53
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 52
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(z, cons(z, nil))  ;  _qaa -> cons(s(z), cons(z, cons(z, nil)))  ;  _raa -> cons(z, cons(z, cons(z, cons(z, nil))))  ;  i -> z  ;  j -> s(z)  ;  l1 -> cons(z, cons(z, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 42, which took 1.292589 s (model generation: 1.291962,  model checking: 0.000627):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7066},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7066
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<cons, nil, cons>(q_gen_7066, q_gen_7031) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<s, z, s>(q_gen_7035) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 53
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 53
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 52
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(s(s(z))), cons(s(s(s(z))), nil))
})

-------------------------------------------
Step 43, which took 1.780688 s (model generation: 1.779095,  model checking: 0.001593):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7035, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7066},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7031
<cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<z, z>() -> q_gen_7032
<s, s>(q_gen_7032) -> q_gen_7035
<s, s>(q_gen_7066) -> q_gen_7035
<s, s>(q_gen_7035) -> q_gen_7066
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<cons, nil, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7035, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7066, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<cons, nil, cons>(q_gen_7066, q_gen_7031) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<s, z, s>(q_gen_7035) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 53
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 53
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 55
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> nil  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 44, which took 1.271765 s (model generation: 1.237211,  model checking: 0.034554):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7051, q_gen_7053, q_gen_7054, q_gen_7074},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7051) -> q_gen_7029
<cons, cons, cons>(q_gen_7074, q_gen_7051) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7074, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7053) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7054, q_gen_7051) -> q_gen_7051
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7051
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<s, s, s>(q_gen_7074) -> q_gen_7074
<z, s, z>(q_gen_7040) -> q_gen_7074
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 53
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 56
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 55
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), nil)  ;  _qaa -> cons(s(s(z)), nil)  ;  _raa -> cons(z, cons(s(z), nil))  ;  i -> s(z)  ;  j -> s(s(z))  ;  l1 -> cons(z, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 45, which took 1.513353 s (model generation: 1.491725,  model checking: 0.021628):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7051, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7073, q_gen_7074},
Q_f={q_gen_7029, q_gen_7051},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7073
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7074, q_gen_7051) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, s, s>(q_gen_7074) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7051
<nil, nil, cons>(q_gen_7073, q_gen_7039) -> q_gen_7051
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7074, q_gen_7052) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7074
<z, s, z>(q_gen_7053) -> q_gen_7074
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 54
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 56
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 58
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(z, cons(z, cons(z, cons(s(z), nil))))  ;  h1 -> z  ;  l2 -> cons(s(z), cons(z, cons(s(s(z)), cons(s(z), nil))))  ;  t1 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 46, which took 2.528825 s (model generation: 2.508353,  model checking: 0.020472):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7074},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7074, q_gen_7052) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7038
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7074, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, s, z>(q_gen_7053) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7052
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7052
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7052
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7054) -> q_gen_7054
<s, s, s>(q_gen_7074) -> q_gen_7074
<z, s, z>(q_gen_7040) -> q_gen_7074
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 55
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 59
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 58
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(s(z)), nil)  ;  _qaa -> cons(z, nil)  ;  _raa -> cons(z, cons(z, nil))  ;  i -> s(s(z))  ;  j -> z  ;  l1 -> cons(z, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 47, which took 5.024390 s (model generation: 5.020914,  model checking: 0.003476):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7038, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7043, q_gen_7044, q_gen_7053, q_gen_7054, q_gen_7074},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7053
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7043
<cons, cons, cons>(q_gen_7041, q_gen_7038) -> q_gen_7029
<cons, cons, cons>(q_gen_7074, q_gen_7044) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7054, q_gen_7038) -> q_gen_7038
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7038
<cons, cons, cons>(q_gen_7074, q_gen_7038) -> q_gen_7038
<cons, nil, cons>(q_gen_7032, q_gen_7043) -> q_gen_7038
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7038
<s, s, s>(q_gen_7054) -> q_gen_7041
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7044
<cons, cons, cons>(q_gen_7041, q_gen_7044) -> q_gen_7044
<cons, cons, cons>(q_gen_7054, q_gen_7044) -> q_gen_7044
<nil, cons, cons>(q_gen_7032, q_gen_7043) -> q_gen_7044
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7044
<s, s, s>(q_gen_7041) -> q_gen_7054
<z, s, z>(q_gen_7053) -> q_gen_7054
<s, s, s>(q_gen_7074) -> q_gen_7074
<z, s, z>(q_gen_7040) -> q_gen_7074
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 56
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 59
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 61
}
Sat witness: Found: ((append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]), {
_jaa -> cons(s(z), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 48, which took 1.817092 s (model generation: 1.619186,  model checking: 0.197906):

Model:
|_
{
append -> 
{{{
Q={q_gen_7029, q_gen_7031, q_gen_7032, q_gen_7039, q_gen_7040, q_gen_7041, q_gen_7052, q_gen_7053, q_gen_7054, q_gen_7055, q_gen_7073, q_gen_7074},
Q_f={q_gen_7029},
Delta=
{
<cons>(q_gen_7040, q_gen_7039) -> q_gen_7039
<nil>() -> q_gen_7039
<z>() -> q_gen_7040
<s>(q_gen_7040) -> q_gen_7053
<s>(q_gen_7053) -> q_gen_7073
<cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7031
<nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7031
<nil, nil>() -> q_gen_7031
<s, s>(q_gen_7032) -> q_gen_7032
<z, z>() -> q_gen_7032
<cons, cons, cons>(q_gen_7041, q_gen_7029) -> q_gen_7029
<cons, cons, cons>(q_gen_7054, q_gen_7052) -> q_gen_7029
<cons, cons, cons>(q_gen_7074, q_gen_7055) -> q_gen_7029
<cons, nil, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, cons, cons>(q_gen_7032, q_gen_7031) -> q_gen_7029
<nil, nil, cons>(q_gen_7040, q_gen_7039) -> q_gen_7029
<nil, nil, nil>() -> q_gen_7029
<s, z, s>(q_gen_7032) -> q_gen_7041
<z, z, z>() -> q_gen_7041
<nil, nil, cons>(q_gen_7053, q_gen_7039) -> q_gen_7052
<s, s, s>(q_gen_7041) -> q_gen_7054
<s, s, s>(q_gen_7074) -> q_gen_7054
<z, s, z>(q_gen_7040) -> q_gen_7054
<cons, cons, cons>(q_gen_7041, q_gen_7052) -> q_gen_7055
<cons, cons, cons>(q_gen_7041, q_gen_7055) -> q_gen_7055
<cons, cons, cons>(q_gen_7054, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7054, q_gen_7055) -> q_gen_7055
<cons, cons, cons>(q_gen_7074, q_gen_7029) -> q_gen_7055
<cons, cons, cons>(q_gen_7074, q_gen_7052) -> q_gen_7055
<nil, nil, cons>(q_gen_7073, q_gen_7039) -> q_gen_7055
<s, s, s>(q_gen_7054) -> q_gen_7074
<z, s, z>(q_gen_7053) -> q_gen_7074
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 57
(append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]) -> 62
(append([t1, l2, _jaa])) -> append([cons(h1, t1), l2, cons(h1, _jaa)]) -> 61
}
Sat witness: Found: ((append([l1, _oaa, _raa]) /\ append([l1, _qaa, _raa]) /\ append([cons(i, nil), l2, _oaa]) /\ append([cons(j, nil), l2, _qaa])) -> eq_nat([i, j]), {
_oaa -> cons(s(z), nil)  ;  _qaa -> cons(s(s(s(z))), nil)  ;  _raa -> cons(s(z), cons(s(z), nil))  ;  i -> s(z)  ;  j -> s(s(s(z)))  ;  l1 -> cons(s(z), nil)  ;  l2 -> cons(z, nil)
})

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