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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(memberl, P:
{() -> memberl([h1, cons(h1, t1)])
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)])
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1])
(memberl([e, nil])) -> BOT}
)
}

properties:
{(memberl([i, l2])) -> memberl([i, l2])}


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

Clause system for inference is:

{
() -> memberl([h1, cons(h1, t1)]) -> 0
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 0
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 0
(memberl([e, nil])) -> BOT -> 0
(memberl([i, l2])) -> memberl([i, l2]) -> 0
}


Solving took 60.001211 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5132, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5136, q_gen_5137, q_gen_5138, q_gen_5139, q_gen_5140, q_gen_5141, q_gen_5142, q_gen_5143, q_gen_5144, q_gen_5145, q_gen_5146, q_gen_5147, q_gen_5148, q_gen_5149, q_gen_5150, q_gen_5151, q_gen_5152, q_gen_5153, q_gen_5154, q_gen_5155, q_gen_5156, q_gen_5157, q_gen_5158, q_gen_5159, q_gen_5160, q_gen_5161, q_gen_5162, q_gen_5163, q_gen_5164, q_gen_5165, q_gen_5166, q_gen_5167, q_gen_5168, q_gen_5169, q_gen_5170, q_gen_5171, q_gen_5172, q_gen_5173, q_gen_5174, q_gen_5175, q_gen_5176, q_gen_5177, q_gen_5178, q_gen_5179, q_gen_5180, q_gen_5181, q_gen_5182, q_gen_5183, q_gen_5184, q_gen_5185, q_gen_5186, q_gen_5187, q_gen_5188, q_gen_5189, q_gen_5190, q_gen_5191, q_gen_5192, q_gen_5193, q_gen_5194, q_gen_5195, q_gen_5196, q_gen_5197, q_gen_5198, q_gen_5199, q_gen_5200, q_gen_5201, q_gen_5202, q_gen_5203, q_gen_5204, q_gen_5205, q_gen_5206, q_gen_5207, q_gen_5208, q_gen_5209, q_gen_5210, q_gen_5211, q_gen_5212, q_gen_5213, q_gen_5214, q_gen_5215, q_gen_5216, q_gen_5217, q_gen_5218, q_gen_5219, q_gen_5220, q_gen_5221, q_gen_5222, q_gen_5223, q_gen_5224, q_gen_5225, q_gen_5226, q_gen_5227, q_gen_5228, q_gen_5229, q_gen_5230, q_gen_5231, q_gen_5232, q_gen_5233, q_gen_5234, q_gen_5235, q_gen_5236, q_gen_5237, q_gen_5238, q_gen_5239, q_gen_5240, q_gen_5241, q_gen_5242, q_gen_5243, q_gen_5244},
Q_f={},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5145
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5148
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5158
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s>(q_gen_5140) -> q_gen_5163
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5165
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5168
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5171
<cons>(q_gen_5163, q_gen_5165) -> q_gen_5175
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5179
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5190
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5212
<cons>(q_gen_5134, q_gen_5212) -> q_gen_5214
<cons>(q_gen_5227, q_gen_5165) -> q_gen_5226
<s>(q_gen_5228) -> q_gen_5227
<s>(q_gen_5229) -> q_gen_5228
<s>(q_gen_5163) -> q_gen_5229
<cons>(q_gen_5163, q_gen_5179) -> q_gen_5234
<cons>(q_gen_5131, q_gen_5190) -> q_gen_5237
<cons>(q_gen_5134, q_gen_5237) -> q_gen_5239
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5132
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5136
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5137
<z, s>(q_gen_5131) -> q_gen_5138
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5139
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5141
<s, cons>(q_gen_5143, q_gen_5130) -> q_gen_5142
<s, s>(q_gen_5138) -> q_gen_5143
<z, cons>(q_gen_5134, q_gen_5145) -> q_gen_5144
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5146
<z, cons>(q_gen_5134, q_gen_5148) -> q_gen_5147
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5149
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5150
<z, s>(q_gen_5134) -> q_gen_5152
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5153
<s, nil>(q_gen_5131) -> q_gen_5154
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5155
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5156
<z, cons>(q_gen_5134, q_gen_5158) -> q_gen_5157
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5159
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5161
<z, cons>(q_gen_5163, q_gen_5133) -> q_gen_5162
<z, cons>(q_gen_5131, q_gen_5165) -> q_gen_5164
<s, cons>(q_gen_5152, q_gen_5165) -> q_gen_5166
<z, cons>(q_gen_5131, q_gen_5168) -> q_gen_5167
<z, cons>(q_gen_5134, q_gen_5168) -> q_gen_5169
<z, cons>(q_gen_5131, q_gen_5171) -> q_gen_5170
<z, cons>(q_gen_5134, q_gen_5165) -> q_gen_5172
<s, cons>(q_gen_5152, q_gen_5171) -> q_gen_5173
<z, cons>(q_gen_5140, q_gen_5175) -> q_gen_5174
<z, cons>(q_gen_5163, q_gen_5165) -> q_gen_5176
<s, cons>(q_gen_5143, q_gen_5160) -> q_gen_5177
<s, cons>(q_gen_5180, q_gen_5179) -> q_gen_5178
<s, z>(q_gen_5131) -> q_gen_5180
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5181
<s, cons>(q_gen_5183, q_gen_5160) -> q_gen_5182
<s, s>(q_gen_5184) -> q_gen_5183
<s, s>(q_gen_5180) -> q_gen_5184
<s, cons>(q_gen_5186, q_gen_5179) -> q_gen_5185
<s, z>(q_gen_5140) -> q_gen_5186
<z, cons>(q_gen_5163, q_gen_5130) -> q_gen_5187
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5188
<s, cons>(q_gen_5152, q_gen_5190) -> q_gen_5189
<z, cons>(q_gen_5140, q_gen_5171) -> q_gen_5191
<s, cons>(q_gen_5193, q_gen_5151) -> q_gen_5192
<z, z>() -> q_gen_5193
<s, cons>(q_gen_5193, q_gen_5130) -> q_gen_5194
<s, cons>(q_gen_5184, q_gen_5160) -> q_gen_5195
<s, cons>(q_gen_5197, q_gen_5190) -> q_gen_5196
<s, z>(q_gen_5134) -> q_gen_5197
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5198
<s, nil>(q_gen_5134) -> q_gen_5199
<s, cons>(q_gen_5138, q_gen_5145) -> q_gen_5200
<s, cons>(q_gen_5138, q_gen_5158) -> q_gen_5201
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5202
<z, cons>(q_gen_5134, q_gen_5190) -> q_gen_5203
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5204
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5205
<s, cons>(q_gen_5207, q_gen_5190) -> q_gen_5206
<s, s>(q_gen_5208) -> q_gen_5207
<s, s>(q_gen_5193) -> q_gen_5208
<s, cons>(q_gen_5207, q_gen_5130) -> q_gen_5209
<s, cons>(q_gen_5197, q_gen_5160) -> q_gen_5210
<z, cons>(q_gen_5131, q_gen_5212) -> q_gen_5211
<s, cons>(q_gen_5215, q_gen_5214) -> q_gen_5213
<s, s>(q_gen_5152) -> q_gen_5215
<s, cons>(q_gen_5208, q_gen_5212) -> q_gen_5216
<z, cons>(q_gen_5134, q_gen_5212) -> q_gen_5217
<s, cons>(q_gen_5186, q_gen_5151) -> q_gen_5218
<s, cons>(q_gen_5220, q_gen_5130) -> q_gen_5219
<s, s>(q_gen_5197) -> q_gen_5220
<s, cons>(q_gen_5222, q_gen_5165) -> q_gen_5221
<s, s>(q_gen_5223) -> q_gen_5222
<s, s>(q_gen_5224) -> q_gen_5223
<s, s>(q_gen_5215) -> q_gen_5224
<s, cons>(q_gen_5230, q_gen_5226) -> q_gen_5225
<s, s>(q_gen_5220) -> q_gen_5230
<s, cons>(q_gen_5208, q_gen_5130) -> q_gen_5231
<s, cons>(q_gen_5207, q_gen_5212) -> q_gen_5232
<s, cons>(q_gen_5180, q_gen_5234) -> q_gen_5233
<s, cons>(q_gen_5215, q_gen_5179) -> q_gen_5235
<s, cons>(q_gen_5138, q_gen_5237) -> q_gen_5236
<s, cons>(q_gen_5193, q_gen_5239) -> q_gen_5238
<s, cons>(q_gen_5152, q_gen_5212) -> q_gen_5240
<s, cons>(q_gen_5193, q_gen_5160) -> q_gen_5241
<s, cons>(q_gen_5215, q_gen_5160) -> q_gen_5242
<s, cons>(q_gen_5193, q_gen_5133) -> q_gen_5243
<z, cons>(q_gen_5131, q_gen_5179) -> q_gen_5244
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.047160 s (model generation: 0.046752,  model checking: 0.000408):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 1
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 1
(memberl([e, nil])) -> BOT -> 1
(memberl([i, l2])) -> memberl([i, l2]) -> 1
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.014336 s (model generation: 0.012803,  model checking: 0.001533):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 2
(memberl([e, nil])) -> BOT -> 2
(memberl([i, l2])) -> memberl([i, l2]) -> 2
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 2, which took 0.010912 s (model generation: 0.010680,  model checking: 0.000232):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<s>(q_gen_5131) -> q_gen_5131
<z>() -> q_gen_5131
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5
(memberl([e, nil])) -> BOT -> 3
(memberl([i, l2])) -> memberl([i, l2]) -> 3
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 3, which took 0.012275 s (model generation: 0.012145,  model checking: 0.000130):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<s>(q_gen_5131) -> q_gen_5131
<z>() -> q_gen_5131
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, nil>() -> q_gen_5129
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 3
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5
(memberl([e, nil])) -> BOT -> 6
(memberl([i, l2])) -> memberl([i, l2]) -> 4
}
Sat witness: Found: ((memberl([e, nil])) -> BOT, {
e -> z
})

-------------------------------------------
Step 4, which took 0.012410 s (model generation: 0.012150,  model checking: 0.000260):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 6
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 4
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5
(memberl([e, nil])) -> BOT -> 6
(memberl([i, l2])) -> memberl([i, l2]) -> 4
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.015646 s (model generation: 0.013910,  model checking: 0.001736):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 6
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 7
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 5
(memberl([e, nil])) -> BOT -> 6
(memberl([i, l2])) -> memberl([i, l2]) -> 5
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 6, which took 0.017730 s (model generation: 0.016279,  model checking: 0.001451):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<s>(q_gen_5134) -> q_gen_5131
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 6
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 7
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 8
(memberl([e, nil])) -> BOT -> 6
(memberl([i, l2])) -> memberl([i, l2]) -> 6
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.014384 s (model generation: 0.013643,  model checking: 0.000741):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 9
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 7
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 8
(memberl([e, nil])) -> BOT -> 7
(memberl([i, l2])) -> memberl([i, l2]) -> 7
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.014734 s (model generation: 0.013167,  model checking: 0.001567):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 9
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 10
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 8
(memberl([e, nil])) -> BOT -> 8
(memberl([i, l2])) -> memberl([i, l2]) -> 8
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 9, which took 0.015381 s (model generation: 0.012270,  model checking: 0.003111):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 12
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 10
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 9
(memberl([e, nil])) -> BOT -> 9
(memberl([i, l2])) -> memberl([i, l2]) -> 9
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 10, which took 0.020617 s (model generation: 0.016636,  model checking: 0.003981):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 12
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 13
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 10
(memberl([e, nil])) -> BOT -> 10
(memberl([i, l2])) -> memberl([i, l2]) -> 10
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 11, which took 0.019990 s (model generation: 0.017269,  model checking: 0.002721):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 13
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 11
(memberl([e, nil])) -> BOT -> 11
(memberl([i, l2])) -> memberl([i, l2]) -> 11
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 12, which took 0.025846 s (model generation: 0.014903,  model checking: 0.010943):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 12
(memberl([e, nil])) -> BOT -> 12
(memberl([i, l2])) -> memberl([i, l2]) -> 12
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 13, which took 0.019446 s (model generation: 0.017868,  model checking: 0.001578):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 15
(memberl([e, nil])) -> BOT -> 13
(memberl([i, l2])) -> memberl([i, l2]) -> 13
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.019020 s (model generation: 0.018530,  model checking: 0.000490):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, nil>(q_gen_5131) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5138
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 15
(memberl([e, nil])) -> BOT -> 16
(memberl([i, l2])) -> memberl([i, l2]) -> 14
}
Sat witness: Found: ((memberl([e, nil])) -> BOT, {
e -> s(z)
})

-------------------------------------------
Step 15, which took 0.022816 s (model generation: 0.021317,  model checking: 0.001499):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 15
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 18
(memberl([e, nil])) -> BOT -> 16
(memberl([i, l2])) -> memberl([i, l2]) -> 15
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 16, which took 0.027694 s (model generation: 0.025282,  model checking: 0.002412):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 18
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 16
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 18
(memberl([e, nil])) -> BOT -> 16
(memberl([i, l2])) -> memberl([i, l2]) -> 16
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 17, which took 0.028524 s (model generation: 0.024106,  model checking: 0.004418):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 18
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 19
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 18
(memberl([e, nil])) -> BOT -> 17
(memberl([i, l2])) -> memberl([i, l2]) -> 17
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(s(z), nil))
})

-------------------------------------------
Step 18, which took 0.026562 s (model generation: 0.023443,  model checking: 0.003119):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5134
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 18
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 19
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 21
(memberl([e, nil])) -> BOT -> 18
(memberl([i, l2])) -> memberl([i, l2]) -> 18
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 19, which took 0.030944 s (model generation: 0.026377,  model checking: 0.004567):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 21
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 19
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 21
(memberl([e, nil])) -> BOT -> 19
(memberl([i, l2])) -> memberl([i, l2]) -> 19
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 20, which took 0.037663 s (model generation: 0.027087,  model checking: 0.010576):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 21
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 22
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 21
(memberl([e, nil])) -> BOT -> 20
(memberl([i, l2])) -> memberl([i, l2]) -> 20
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(s(s(z)))  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 21, which took 0.082258 s (model generation: 0.025985,  model checking: 0.056273):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 22
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 22
(memberl([e, nil])) -> BOT -> 21
(memberl([i, l2])) -> memberl([i, l2]) -> 21
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 22, which took 0.255407 s (model generation: 0.029021,  model checking: 0.226386):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5130
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 24
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 23
(memberl([e, nil])) -> BOT -> 22
(memberl([i, l2])) -> memberl([i, l2]) -> 22
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 23, which took 0.097684 s (model generation: 0.031849,  model checking: 0.065835):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 25
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 24
(memberl([e, nil])) -> BOT -> 23
(memberl([i, l2])) -> memberl([i, l2]) -> 23
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 24, which took 0.147014 s (model generation: 0.032948,  model checking: 0.114066):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 27
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 25
(memberl([e, nil])) -> BOT -> 24
(memberl([i, l2])) -> memberl([i, l2]) -> 24
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 25, which took 0.135192 s (model generation: 0.037515,  model checking: 0.097677):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 26
(memberl([e, nil])) -> BOT -> 25
(memberl([i, l2])) -> memberl([i, l2]) -> 25
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 26, which took 0.042343 s (model generation: 0.037475,  model checking: 0.004868):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 28
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 29
(memberl([e, nil])) -> BOT -> 26
(memberl([i, l2])) -> memberl([i, l2]) -> 26
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 27, which took 0.050582 s (model generation: 0.041202,  model checking: 0.009380):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 31
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 29
(memberl([e, nil])) -> BOT -> 27
(memberl([i, l2])) -> memberl([i, l2]) -> 27
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 28, which took 0.051839 s (model generation: 0.043346,  model checking: 0.008493):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 30
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 31
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 32
(memberl([e, nil])) -> BOT -> 28
(memberl([i, l2])) -> memberl([i, l2]) -> 28
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(s(z))), cons(s(z), cons(s(z), nil)))
})

-------------------------------------------
Step 29, which took 0.059743 s (model generation: 0.050590,  model checking: 0.009153):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 31
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 34
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 32
(memberl([e, nil])) -> BOT -> 29
(memberl([i, l2])) -> memberl([i, l2]) -> 29
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(s(z)), nil))
})

-------------------------------------------
Step 30, which took 0.064292 s (model generation: 0.059567,  model checking: 0.004725):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 32
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 34
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 35
(memberl([e, nil])) -> BOT -> 30
(memberl([i, l2])) -> memberl([i, l2]) -> 30
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 31, which took 0.141519 s (model generation: 0.059532,  model checking: 0.081987):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<s>(q_gen_5140) -> q_gen_5131
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 33
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 37
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 35
(memberl([e, nil])) -> BOT -> 31
(memberl([i, l2])) -> memberl([i, l2]) -> 31
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(s(s(z))))  ;  h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(s(z)), nil))
})

-------------------------------------------
Step 32, which took 0.070356 s (model generation: 0.066114,  model checking: 0.004242):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<s>(q_gen_5140) -> q_gen_5131
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 34
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 37
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 38
(memberl([e, nil])) -> BOT -> 32
(memberl([i, l2])) -> memberl([i, l2]) -> 32
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(s(z)))  ;  t1 -> nil
})

-------------------------------------------
Step 33, which took 0.080506 s (model generation: 0.069291,  model checking: 0.011215):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 35
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 40
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 38
(memberl([e, nil])) -> BOT -> 33
(memberl([i, l2])) -> memberl([i, l2]) -> 33
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(s(s(z)), nil))
})

-------------------------------------------
Step 34, which took 0.084026 s (model generation: 0.077625,  model checking: 0.006401):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 36
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 40
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 41
(memberl([e, nil])) -> BOT -> 34
(memberl([i, l2])) -> memberl([i, l2]) -> 34
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 35, which took 0.096538 s (model generation: 0.082738,  model checking: 0.013800):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 37
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 43
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 41
(memberl([e, nil])) -> BOT -> 35
(memberl([i, l2])) -> memberl([i, l2]) -> 35
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 36, which took 0.090071 s (model generation: 0.086142,  model checking: 0.003929):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, z>() -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 38
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 43
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 44
(memberl([e, nil])) -> BOT -> 36
(memberl([i, l2])) -> memberl([i, l2]) -> 36
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 37, which took 0.105694 s (model generation: 0.091151,  model checking: 0.014543):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 39
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 44
(memberl([e, nil])) -> BOT -> 37
(memberl([i, l2])) -> memberl([i, l2]) -> 37
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(s(z)))  ;  h1 -> z  ;  t1 -> cons(s(z), cons(s(s(z)), nil))
})

-------------------------------------------
Step 38, which took 0.108911 s (model generation: 0.098870,  model checking: 0.010041):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 40
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 47
(memberl([e, nil])) -> BOT -> 38
(memberl([i, l2])) -> memberl([i, l2]) -> 38
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 39, which took 0.120306 s (model generation: 0.117520,  model checking: 0.002786):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, nil>(q_gen_5134) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 40
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 47
(memberl([e, nil])) -> BOT -> 41
(memberl([i, l2])) -> memberl([i, l2]) -> 39
}
Sat witness: Found: ((memberl([e, nil])) -> BOT, {
e -> s(s(z))
})

-------------------------------------------
Step 40, which took 1.421181 s (model generation: 0.109863,  model checking: 1.311318):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5145, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5134, q_gen_5145) -> q_gen_5130
<cons>(q_gen_5140, q_gen_5145) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5145
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5145
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5145) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5145) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5145) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5152
<s, z>(q_gen_5134) -> q_gen_5152
<s, z>(q_gen_5140) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 43
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 47
(memberl([e, nil])) -> BOT -> 41
(memberl([i, l2])) -> memberl([i, l2]) -> 40
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 41, which took 0.126956 s (model generation: 0.117322,  model checking: 0.009634):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5158},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5134, q_gen_5158) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5158) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5158
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5158
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5158) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5158) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5158) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 46
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 46
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 47
(memberl([e, nil])) -> BOT -> 42
(memberl([i, l2])) -> memberl([i, l2]) -> 41
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(z, cons(s(z), nil))
})

-------------------------------------------
Step 42, which took 0.128536 s (model generation: 0.118747,  model checking: 0.009789):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5145, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5145
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5145
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5145) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5145) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5145) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5145) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5145) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 46
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 49
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 47
(memberl([e, nil])) -> BOT -> 43
(memberl([i, l2])) -> memberl([i, l2]) -> 42
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(z), cons(s(s(z)), nil))
})

-------------------------------------------
Step 43, which took 0.172950 s (model generation: 0.167466,  model checking: 0.005484):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5152
<s, z>(q_gen_5134) -> q_gen_5152
<s, z>(q_gen_5140) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 49
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 49
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 47
(memberl([e, nil])) -> BOT -> 44
(memberl([i, l2])) -> memberl([i, l2]) -> 43
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 44, which took 0.147676 s (model generation: 0.140176,  model checking: 0.007500):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5145, q_gen_5151, q_gen_5152},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5145
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5145
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5145
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5145) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5145) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5145) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5145) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5145) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5152
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 49
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 49
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 50
(memberl([e, nil])) -> BOT -> 45
(memberl([i, l2])) -> memberl([i, l2]) -> 44
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 45, which took 0.166650 s (model generation: 0.152085,  model checking: 0.014565):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5131) -> q_gen_5152
<s, z>(q_gen_5140) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 49
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 52
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 50
(memberl([e, nil])) -> BOT -> 46
(memberl([i, l2])) -> memberl([i, l2]) -> 45
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 46, which took 0.197083 s (model generation: 0.190837,  model checking: 0.006246):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
<z, z>() -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 52
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 52
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 50
(memberl([e, nil])) -> BOT -> 47
(memberl([i, l2])) -> memberl([i, l2]) -> 46
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 47, which took 0.180025 s (model generation: 0.155486,  model checking: 0.024539):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5152
<s, z>(q_gen_5140) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 52
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 52
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 53
(memberl([e, nil])) -> BOT -> 48
(memberl([i, l2])) -> memberl([i, l2]) -> 47
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(s(z)))  ;  h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(s(s(z)), nil))
})

-------------------------------------------
Step 48, which took 0.187342 s (model generation: 0.168703,  model checking: 0.018639):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 52
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 55
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 53
(memberl([e, nil])) -> BOT -> 49
(memberl([i, l2])) -> memberl([i, l2]) -> 48
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(s(z)))  ;  h1 -> z  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 49, which took 0.199994 s (model generation: 0.193822,  model checking: 0.006172):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 55
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 55
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 53
(memberl([e, nil])) -> BOT -> 50
(memberl([i, l2])) -> memberl([i, l2]) -> 49
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(z, cons(s(s(z)), nil))
})

-------------------------------------------
Step 50, which took 0.202323 s (model generation: 0.174575,  model checking: 0.027748):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5130
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 55
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 55
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 56
(memberl([e, nil])) -> BOT -> 51
(memberl([i, l2])) -> memberl([i, l2]) -> 50
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(z))  ;  h1 -> s(s(s(z)))  ;  t1 -> cons(s(z), cons(z, cons(s(s(z)), nil)))
})

-------------------------------------------
Step 51, which took 0.218850 s (model generation: 0.204849,  model checking: 0.014001):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<s, s>(q_gen_5152) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
<z, z>() -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 55
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 58
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 56
(memberl([e, nil])) -> BOT -> 52
(memberl([i, l2])) -> memberl([i, l2]) -> 51
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(s(s(z)), nil))
})

-------------------------------------------
Step 52, which took 0.241537 s (model generation: 0.212114,  model checking: 0.029423):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5152) -> q_gen_5180
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 56
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 58
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 59
(memberl([e, nil])) -> BOT -> 53
(memberl([i, l2])) -> memberl([i, l2]) -> 52
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(s(s(z))))  ;  h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 53, which took 0.255789 s (model generation: 0.222272,  model checking: 0.033517):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 57
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 61
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 59
(memberl([e, nil])) -> BOT -> 54
(memberl([i, l2])) -> memberl([i, l2]) -> 53
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(s(s(s(z)))))  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(s(s(s(s(z)))))), cons(s(z), cons(s(z), nil)))
})

-------------------------------------------
Step 54, which took 0.437961 s (model generation: 0.423586,  model checking: 0.014375):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
<z, z>() -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 58
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 61
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 62
(memberl([e, nil])) -> BOT -> 55
(memberl([i, l2])) -> memberl([i, l2]) -> 54
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(z))  ;  h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 55, which took 0.287369 s (model generation: 0.272448,  model checking: 0.014921):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5152
<s, z>(q_gen_5140) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<s, s>(q_gen_5152) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<z, z>() -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 59
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 64
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 62
(memberl([e, nil])) -> BOT -> 56
(memberl([i, l2])) -> memberl([i, l2]) -> 55
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(s(z)))  ;  h1 -> s(s(z))  ;  t1 -> cons(z, cons(s(s(z)), nil))
})

-------------------------------------------
Step 56, which took 0.333483 s (model generation: 0.303851,  model checking: 0.029632):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 60
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 64
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 65
(memberl([e, nil])) -> BOT -> 57
(memberl([i, l2])) -> memberl([i, l2]) -> 56
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(z))  ;  h1 -> z  ;  t1 -> cons(s(s(s(z))), cons(s(s(z)), cons(s(s(z)), nil)))
})

-------------------------------------------
Step 57, which took 0.342843 s (model generation: 0.322275,  model checking: 0.020568):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5134) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5140) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 61
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 67
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 65
(memberl([e, nil])) -> BOT -> 58
(memberl([i, l2])) -> memberl([i, l2]) -> 57
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(z), cons(z, cons(s(z), cons(s(s(z)), nil))))
})

-------------------------------------------
Step 58, which took 0.419299 s (model generation: 0.403410,  model checking: 0.015889):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5152) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 62
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 67
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 68
(memberl([e, nil])) -> BOT -> 59
(memberl([i, l2])) -> memberl([i, l2]) -> 58
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> s(s(z))  ;  t1 -> cons(z, cons(s(s(z)), nil))
})

-------------------------------------------
Step 59, which took 0.420813 s (model generation: 0.406459,  model checking: 0.014354):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<s, s>(q_gen_5152) -> q_gen_5152
<s, z>(q_gen_5140) -> q_gen_5152
<z, s>(q_gen_5134) -> q_gen_5152
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<z, z>() -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 63
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 70
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 68
(memberl([e, nil])) -> BOT -> 60
(memberl([i, l2])) -> memberl([i, l2]) -> 59
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> s(s(z))  ;  h1 -> s(s(s(z)))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 60, which took 0.991412 s (model generation: 0.972868,  model checking: 0.018544):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5140) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, z>(q_gen_5134) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
<s, s>(q_gen_5152) -> q_gen_5180
<s, s>(q_gen_5180) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<z, z>() -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 64
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 70
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 71
(memberl([e, nil])) -> BOT -> 61
(memberl([i, l2])) -> memberl([i, l2]) -> 60
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 61, which took 1.097684 s (model generation: 1.088837,  model checking: 0.008847):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_5129, q_gen_5130, q_gen_5131, q_gen_5133, q_gen_5134, q_gen_5135, q_gen_5138, q_gen_5140, q_gen_5151, q_gen_5152, q_gen_5160, q_gen_5179, q_gen_5180},
Q_f={q_gen_5129},
Delta=
{
<nil>() -> q_gen_5130
<z>() -> q_gen_5131
<cons>(q_gen_5131, q_gen_5130) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5151) -> q_gen_5133
<cons>(q_gen_5131, q_gen_5160) -> q_gen_5133
<cons>(q_gen_5134, q_gen_5133) -> q_gen_5133
<cons>(q_gen_5140, q_gen_5133) -> q_gen_5133
<s>(q_gen_5131) -> q_gen_5134
<s>(q_gen_5134) -> q_gen_5140
<s>(q_gen_5140) -> q_gen_5140
<cons>(q_gen_5134, q_gen_5130) -> q_gen_5151
<cons>(q_gen_5134, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5151) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5179) -> q_gen_5151
<cons>(q_gen_5140, q_gen_5130) -> q_gen_5160
<cons>(q_gen_5131, q_gen_5179) -> q_gen_5179
<cons>(q_gen_5134, q_gen_5160) -> q_gen_5179
<cons>(q_gen_5134, q_gen_5179) -> q_gen_5179
<cons>(q_gen_5140, q_gen_5160) -> q_gen_5179
<s, cons>(q_gen_5138, q_gen_5130) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5138, q_gen_5179) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5151) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5179) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5160) -> q_gen_5129
<s, cons>(q_gen_5180, q_gen_5179) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5130) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5151) -> q_gen_5129
<z, cons>(q_gen_5131, q_gen_5160) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5133) -> q_gen_5129
<z, cons>(q_gen_5134, q_gen_5179) -> q_gen_5129
<z, cons>(q_gen_5140, q_gen_5133) -> q_gen_5129
<s, cons>(q_gen_5152, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5152, q_gen_5160) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5130) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5133) -> q_gen_5135
<s, cons>(q_gen_5180, q_gen_5151) -> q_gen_5135
<s, nil>(q_gen_5131) -> q_gen_5135
<s, nil>(q_gen_5134) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5151) -> q_gen_5135
<z, cons>(q_gen_5134, q_gen_5160) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5130) -> q_gen_5135
<z, cons>(q_gen_5140, q_gen_5151) -> q_gen_5135
<z, nil>() -> q_gen_5135
<s, s>(q_gen_5138) -> q_gen_5138
<s, s>(q_gen_5180) -> q_gen_5138
<s, z>(q_gen_5140) -> q_gen_5138
<z, s>(q_gen_5131) -> q_gen_5138
<z, s>(q_gen_5134) -> q_gen_5152
<z, z>() -> q_gen_5152
<s, s>(q_gen_5152) -> q_gen_5180
<s, z>(q_gen_5131) -> q_gen_5180
<s, z>(q_gen_5134) -> q_gen_5180
}

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

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

Teacher's answer:
New clause system:
{
() -> memberl([h1, cons(h1, t1)]) -> 67
(memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]) -> 70
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 71
(memberl([e, nil])) -> BOT -> 62
(memberl([i, l2])) -> memberl([i, l2]) -> 61
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(s(z)), cons(s(s(z)), nil))
})

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