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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)])}
(append([_hw, _iw, _jw]) /\ append([_hw, _iw, _kw])) -> eq_natlist([_jw, _kw])
)
}

properties:
{(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 0
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 0
}


Solving took 60.000074 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4125, q_gen_4126, q_gen_4127, q_gen_4128, q_gen_4129, q_gen_4130, q_gen_4131, q_gen_4132, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4137, q_gen_4138, q_gen_4139, q_gen_4140, q_gen_4141, q_gen_4142, q_gen_4143, q_gen_4144, q_gen_4145, q_gen_4146, q_gen_4147, q_gen_4148, q_gen_4149, q_gen_4150, q_gen_4151, q_gen_4152, q_gen_4153, q_gen_4154, q_gen_4155, q_gen_4156, q_gen_4157, q_gen_4158, q_gen_4159, q_gen_4160, q_gen_4161, q_gen_4162, q_gen_4163, q_gen_4164, q_gen_4165, q_gen_4166, q_gen_4167, q_gen_4168, q_gen_4169, q_gen_4170, q_gen_4171, q_gen_4172, q_gen_4173, q_gen_4174, q_gen_4175, q_gen_4176, q_gen_4177, q_gen_4178, q_gen_4179, q_gen_4180, q_gen_4181, q_gen_4182, q_gen_4183, q_gen_4184, q_gen_4185, q_gen_4186, q_gen_4187, q_gen_4188, q_gen_4189, q_gen_4190, q_gen_4191, q_gen_4192, q_gen_4193, q_gen_4194, q_gen_4195, q_gen_4196},
Q_f={},
Delta=
{
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4142
<s>(q_gen_4135) -> q_gen_4148
<s>(q_gen_4148) -> q_gen_4168
<cons>(q_gen_4135, q_gen_4185) -> q_gen_4184
<cons>(q_gen_4168, q_gen_4134) -> q_gen_4185
<s>(q_gen_4168) -> q_gen_4186
<nil, nil>() -> q_gen_4126
<z, z>() -> q_gen_4127
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4129
<s, s>(q_gen_4127) -> q_gen_4130
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4138
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4156
<cons, cons>(q_gen_4160, q_gen_4126) -> q_gen_4159
<s, s>(q_gen_4130) -> q_gen_4160
<nil, nil, nil>() -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4125
<nil, cons, cons>(q_gen_4130, q_gen_4129) -> q_gen_4128
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4131
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4132
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<z, z, z>() -> q_gen_4136
<cons, nil, cons>(q_gen_4127, q_gen_4138) -> q_gen_4137
<nil, cons, cons>(q_gen_4127, q_gen_4138) -> q_gen_4139
<cons, cons, cons>(q_gen_4136, q_gen_4141) -> q_gen_4140
<nil, nil, cons>(q_gen_4135, q_gen_4142) -> q_gen_4141
<cons, cons, cons>(q_gen_4144, q_gen_4141) -> q_gen_4143
<s, z, s>(q_gen_4127) -> q_gen_4144
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4145
<cons, cons, cons>(q_gen_4149, q_gen_4147) -> q_gen_4146
<nil, nil, cons>(q_gen_4148, q_gen_4134) -> q_gen_4147
<s, s, s>(q_gen_4136) -> q_gen_4149
<cons, cons, cons>(q_gen_4149, q_gen_4124) -> q_gen_4150
<cons, cons, cons>(q_gen_4144, q_gen_4124) -> q_gen_4151
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4152
<cons, cons, cons>(q_gen_4149, q_gen_4133) -> q_gen_4153
<cons, cons, cons>(q_gen_4144, q_gen_4133) -> q_gen_4154
<nil, cons, cons>(q_gen_4127, q_gen_4156) -> q_gen_4155
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4157
<nil, cons, cons>(q_gen_4160, q_gen_4159) -> q_gen_4158
<cons, cons, cons>(q_gen_4149, q_gen_4157) -> q_gen_4161
<cons, cons, cons>(q_gen_4144, q_gen_4157) -> q_gen_4162
<cons, nil, cons>(q_gen_4130, q_gen_4138) -> q_gen_4163
<cons, cons, cons>(q_gen_4149, q_gen_4125) -> q_gen_4164
<nil, cons, cons>(q_gen_4160, q_gen_4126) -> q_gen_4165
<cons, cons, cons>(q_gen_4169, q_gen_4167) -> q_gen_4166
<nil, nil, cons>(q_gen_4168, q_gen_4134) -> q_gen_4167
<s, s, s>(q_gen_4170) -> q_gen_4169
<z, s, z>(q_gen_4135) -> q_gen_4170
<cons, cons, cons>(q_gen_4172, q_gen_4147) -> q_gen_4171
<s, s, s>(q_gen_4149) -> q_gen_4172
<cons, cons, cons>(q_gen_4174, q_gen_4147) -> q_gen_4173
<s, s, s>(q_gen_4144) -> q_gen_4174
<cons, cons, cons>(q_gen_4176, q_gen_4124) -> q_gen_4175
<s, z, s>(q_gen_4130) -> q_gen_4176
<cons, cons, cons>(q_gen_4170, q_gen_4124) -> q_gen_4177
<cons, cons, cons>(q_gen_4176, q_gen_4133) -> q_gen_4178
<cons, cons, cons>(q_gen_4180, q_gen_4175) -> q_gen_4179
<z, s, z>(q_gen_4148) -> q_gen_4180
<cons, cons, cons>(q_gen_4170, q_gen_4175) -> q_gen_4181
<cons, cons, cons>(q_gen_4149, q_gen_4183) -> q_gen_4182
<nil, nil, cons>(q_gen_4186, q_gen_4184) -> q_gen_4183
<cons, cons, cons>(q_gen_4170, q_gen_4188) -> q_gen_4187
<cons, cons, cons>(q_gen_4191, q_gen_4189) -> q_gen_4188
<cons, cons, cons>(q_gen_4136, q_gen_4190) -> q_gen_4189
<cons, cons, cons>(q_gen_4180, q_gen_4124) -> q_gen_4190
<s, s, s>(q_gen_4180) -> q_gen_4191
<cons, cons, cons>(q_gen_4136, q_gen_4193) -> q_gen_4192
<cons, cons, cons>(q_gen_4191, q_gen_4194) -> q_gen_4193
<cons, nil, cons>(q_gen_4127, q_gen_4156) -> q_gen_4194
<cons, cons, cons>(q_gen_4170, q_gen_4196) -> q_gen_4195
<nil, nil, cons>(q_gen_4186, q_gen_4134) -> q_gen_4196
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.006921 s (model generation: 0.006567,  model checking: 0.000354):

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.006610 s (model generation: 0.006241,  model checking: 0.000369):

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

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

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

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

-------------------------------------------
Step 2, which took 0.005645 s (model generation: 0.005232,  model checking: 0.000413):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127},
Q_f={q_gen_4124},
Delta=
{
<nil, nil>() -> q_gen_4126
<z, z>() -> q_gen_4127
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
}

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

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

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

-------------------------------------------
Step 3, which took 0.006945 s (model generation: 0.005451,  model checking: 0.001494):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127},
Q_f={q_gen_4124},
Delta=
{
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
}

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

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

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

-------------------------------------------
Step 4, which took 0.010118 s (model generation: 0.007005,  model checking: 0.003113):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 5, which took 0.011403 s (model generation: 0.006900,  model checking: 0.004503):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 6, which took 0.014593 s (model generation: 0.009207,  model checking: 0.005386):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 7, which took 0.014378 s (model generation: 0.008511,  model checking: 0.005867):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 8, which took 0.011229 s (model generation: 0.009321,  model checking: 0.001908):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 9, which took 0.012403 s (model generation: 0.010502,  model checking: 0.001901):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4133
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 10, which took 0.014989 s (model generation: 0.014458,  model checking: 0.000531):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4152},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4152
}

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

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

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

-------------------------------------------
Step 11, which took 0.016614 s (model generation: 0.012915,  model checking: 0.003699):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4152},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4152
}

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

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

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

-------------------------------------------
Step 12, which took 0.012869 s (model generation: 0.012468,  model checking: 0.000401):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4133
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4133
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
}

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

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

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

-------------------------------------------
Step 13, which took 0.020424 s (model generation: 0.019000,  model checking: 0.001424):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4129, q_gen_4131, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4129
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4129) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4131
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4131
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 17
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 19
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

-------------------------------------------
Step 14, which took 0.041095 s (model generation: 0.037814,  model checking: 0.003281):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<s, s>(q_gen_4130) -> q_gen_4130
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4133
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4133
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 20
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 19
}
Sat witness: Found: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(s(z), cons(z, nil))  ;  _nw -> cons(z, cons(z, nil))  ;  _ow -> cons(s(z), cons(z, nil))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(s(z), cons(z, nil))  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 15, which took 0.025911 s (model generation: 0.025375,  model checking: 0.000536):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4125, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4150},
Q_f={q_gen_4124, q_gen_4125},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4130) -> q_gen_4127
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4125) -> q_gen_4125
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4125
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4125
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4125
<s, s, s>(q_gen_4136) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4150
<cons, cons, cons>(q_gen_4136, q_gen_4150) -> q_gen_4150
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4150
}

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

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

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

-------------------------------------------
Step 16, which took 0.037447 s (model generation: 0.021575,  model checking: 0.015872):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4148, q_gen_4149},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<s>(q_gen_4135) -> q_gen_4148
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4124
<cons, cons, cons>(q_gen_4149, q_gen_4124) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4148, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4133
<cons, cons, cons>(q_gen_4149, q_gen_4133) -> q_gen_4133
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<s, s, s>(q_gen_4136) -> q_gen_4149
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 23
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 22
}
Sat witness: Found: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(z, cons(z, nil))  ;  _nw -> cons(s(z), nil)  ;  _ow -> cons(s(z), cons(z, nil))  ;  i -> z  ;  j -> s(z)  ;  l1 -> cons(s(z), cons(z, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 17, which took 0.062765 s (model generation: 0.039889,  model checking: 0.022876):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4147, q_gen_4148, q_gen_4149},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<s>(q_gen_4135) -> q_gen_4148
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, cons, cons>(q_gen_4149, q_gen_4147) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, cons, cons>(q_gen_4149, q_gen_4124) -> q_gen_4147
<nil, nil, cons>(q_gen_4148, q_gen_4134) -> q_gen_4147
<s, s, s>(q_gen_4136) -> q_gen_4149
}

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

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

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

-------------------------------------------
Step 18, which took 0.115405 s (model generation: 0.072541,  model checking: 0.042864):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4147, q_gen_4148, q_gen_4149},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<s>(q_gen_4135) -> q_gen_4148
<s>(q_gen_4148) -> q_gen_4148
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, cons, cons>(q_gen_4149, q_gen_4147) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, cons, cons>(q_gen_4149, q_gen_4124) -> q_gen_4147
<nil, nil, cons>(q_gen_4148, q_gen_4134) -> q_gen_4147
<s, s, s>(q_gen_4136) -> q_gen_4149
<s, s, s>(q_gen_4149) -> q_gen_4149
<z, s, z>(q_gen_4135) -> q_gen_4149
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 26
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 25
}
Sat witness: Found: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(s(z), nil)  ;  _nw -> cons(s(s(z)), nil)  ;  _ow -> cons(s(s(z)), cons(s(z), nil))  ;  i -> s(z)  ;  j -> s(s(z))  ;  l1 -> cons(s(s(z)), nil)  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 19, which took 0.079052 s (model generation: 0.077533,  model checking: 0.001519):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4147, q_gen_4148, q_gen_4149},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<z>() -> q_gen_4135
<s>(q_gen_4135) -> q_gen_4148
<s>(q_gen_4148) -> q_gen_4148
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, cons, cons>(q_gen_4149, q_gen_4147) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, s, s>(q_gen_4149) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, s, z>(q_gen_4135) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, cons, cons>(q_gen_4136, q_gen_4147) -> q_gen_4147
<cons, cons, cons>(q_gen_4149, q_gen_4124) -> q_gen_4147
<nil, nil, cons>(q_gen_4148, q_gen_4134) -> q_gen_4147
<s, s, s>(q_gen_4136) -> q_gen_4149
}

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

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

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

-------------------------------------------
Step 20, which took 0.163500 s (model generation: 0.088755,  model checking: 0.074745):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4144},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4130) -> q_gen_4127
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4124
<cons, cons, cons>(q_gen_4144, q_gen_4133) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4144, q_gen_4124) -> q_gen_4133
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4133
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<s, s, s>(q_gen_4136) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<s, s, s>(q_gen_4144) -> q_gen_4144
<s, z, s>(q_gen_4127) -> q_gen_4144
<s, z, s>(q_gen_4130) -> q_gen_4144
<z, s, z>(q_gen_4135) -> q_gen_4144
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 29
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 28
}
Sat witness: Found: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(s(z), cons(z, nil))  ;  _nw -> cons(s(s(z)), cons(z, nil))  ;  _ow -> cons(z, cons(s(s(z)), nil))  ;  i -> s(z)  ;  j -> s(s(z))  ;  l1 -> cons(z, cons(s(s(z)), nil))  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 21, which took 0.101964 s (model generation: 0.101120,  model checking: 0.000844):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4130, q_gen_4133, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4144},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4135) -> q_gen_4135
<z>() -> q_gen_4135
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4130) -> q_gen_4127
<z, z>() -> q_gen_4127
<s, s>(q_gen_4127) -> q_gen_4130
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, cons, cons>(q_gen_4136, q_gen_4133) -> q_gen_4124
<cons, cons, cons>(q_gen_4144, q_gen_4133) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4130, q_gen_4126) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<cons, cons, cons>(q_gen_4144, q_gen_4124) -> q_gen_4133
<cons, nil, cons>(q_gen_4130, q_gen_4126) -> q_gen_4133
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4133
<s, z, s>(q_gen_4130) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<s, s, s>(q_gen_4136) -> q_gen_4144
<s, s, s>(q_gen_4144) -> q_gen_4144
<s, z, s>(q_gen_4127) -> q_gen_4144
<z, s, z>(q_gen_4135) -> q_gen_4144
}

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

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

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

-------------------------------------------
Step 22, which took 0.105761 s (model generation: 0.078823,  model checking: 0.026938):

Model:
|_
{
append -> 
{{{
Q={q_gen_4124, q_gen_4126, q_gen_4127, q_gen_4134, q_gen_4135, q_gen_4136, q_gen_4147, q_gen_4148, q_gen_4149},
Q_f={q_gen_4124},
Delta=
{
<cons>(q_gen_4135, q_gen_4134) -> q_gen_4134
<nil>() -> q_gen_4134
<s>(q_gen_4148) -> q_gen_4135
<z>() -> q_gen_4135
<s>(q_gen_4135) -> q_gen_4148
<cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4126
<nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4126
<nil, nil>() -> q_gen_4126
<s, s>(q_gen_4127) -> q_gen_4127
<z, z>() -> q_gen_4127
<cons, cons, cons>(q_gen_4136, q_gen_4124) -> q_gen_4124
<cons, cons, cons>(q_gen_4149, q_gen_4147) -> q_gen_4124
<cons, nil, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, cons, cons>(q_gen_4127, q_gen_4126) -> q_gen_4124
<nil, nil, cons>(q_gen_4135, q_gen_4134) -> q_gen_4124
<nil, nil, nil>() -> q_gen_4124
<s, s, s>(q_gen_4149) -> q_gen_4136
<s, z, s>(q_gen_4127) -> q_gen_4136
<z, z, z>() -> q_gen_4136
<cons, cons, cons>(q_gen_4136, q_gen_4147) -> q_gen_4147
<cons, cons, cons>(q_gen_4149, q_gen_4124) -> q_gen_4147
<nil, nil, cons>(q_gen_4148, q_gen_4134) -> q_gen_4147
<s, s, s>(q_gen_4136) -> q_gen_4149
<z, s, z>(q_gen_4135) -> q_gen_4149
<z, s, z>(q_gen_4148) -> q_gen_4149
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
(append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]) -> 32
(append([t1, l2, _gw])) -> append([cons(h1, t1), l2, cons(h1, _gw)]) -> 31
}
Sat witness: Found: ((append([l1, _lw, _ow]) /\ append([l1, _nw, _ow]) /\ append([cons(i, nil), l2, _lw]) /\ append([cons(j, nil), l2, _nw])) -> eq_nat([i, j]), {
_lw -> cons(s(z), cons(s(s(s(z))), cons(z, cons(s(s(z)), nil))))  ;  _nw -> cons(z, cons(s(s(s(z))), nil))  ;  _ow -> cons(z, cons(s(z), cons(z, cons(z, nil))))  ;  i -> s(z)  ;  j -> z  ;  l1 -> cons(z, cons(s(z), cons(z, cons(z, nil))))  ;  l2 -> cons(s(z), nil)
})

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