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


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.000408 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1110, q_gen_1111, q_gen_1112, q_gen_1113, q_gen_1114, q_gen_1115, q_gen_1116, q_gen_1117, q_gen_1118, q_gen_1119, q_gen_1120, q_gen_1121, q_gen_1122, q_gen_1123, q_gen_1124, q_gen_1125, q_gen_1126, q_gen_1127, q_gen_1128, q_gen_1129, q_gen_1130, q_gen_1131, q_gen_1132, q_gen_1133, q_gen_1134, q_gen_1135, q_gen_1136, q_gen_1137, q_gen_1138, q_gen_1139, q_gen_1140, q_gen_1141, q_gen_1142, q_gen_1143, q_gen_1144, q_gen_1145, q_gen_1146, q_gen_1147, q_gen_1148, q_gen_1149, q_gen_1150, q_gen_1151, q_gen_1152, q_gen_1153, q_gen_1154, q_gen_1155, q_gen_1156, q_gen_1157, q_gen_1158, q_gen_1159, q_gen_1160, q_gen_1161, q_gen_1162, q_gen_1163, q_gen_1164, q_gen_1165, q_gen_1166, q_gen_1167},
Q_f={},
Delta=
{
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1115
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1118
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1120
<s>(q_gen_1113) -> q_gen_1136
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1141
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1110
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1111
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1112
<z, cons>(q_gen_1105, q_gen_1115) -> q_gen_1114
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
<z, cons>(q_gen_1108, q_gen_1118) -> q_gen_1117
<z, cons>(q_gen_1105, q_gen_1120) -> q_gen_1119
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1121
<z, cons>(q_gen_1108, q_gen_1115) -> q_gen_1122
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1123
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1124
<s, cons>(q_gen_1105, q_gen_1110) -> q_gen_1125
<s, cons>(q_gen_1108, q_gen_1110) -> q_gen_1126
<s, nil>(q_gen_1105) -> q_gen_1127
<s, cons>(q_gen_1105, q_gen_1129) -> q_gen_1128
<s, cons>(q_gen_1108, q_gen_1130) -> q_gen_1129
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1130
<s, cons>(q_gen_1105, q_gen_1132) -> q_gen_1131
<s, cons>(q_gen_1105, q_gen_1133) -> q_gen_1132
<s, cons>(q_gen_1108, q_gen_1122) -> q_gen_1133
<s, cons>(q_gen_1136, q_gen_1135) -> q_gen_1134
<s, nil>(q_gen_1108) -> q_gen_1135
<z, cons>(q_gen_1108, q_gen_1120) -> q_gen_1137
<s, cons>(q_gen_1113, q_gen_1110) -> q_gen_1138
<s, cons>(q_gen_1113, q_gen_1124) -> q_gen_1139
<z, cons>(q_gen_1113, q_gen_1141) -> q_gen_1140
<s, cons>(q_gen_1108, q_gen_1143) -> q_gen_1142
<s, cons>(q_gen_1105, q_gen_1144) -> q_gen_1143
<s, cons>(q_gen_1105, q_gen_1145) -> q_gen_1144
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1145
<s, cons>(q_gen_1105, q_gen_1147) -> q_gen_1146
<s, cons>(q_gen_1105, q_gen_1148) -> q_gen_1147
<s, cons>(q_gen_1105, q_gen_1138) -> q_gen_1148
<s, cons>(q_gen_1108, q_gen_1125) -> q_gen_1149
<s, cons>(q_gen_1105, q_gen_1121) -> q_gen_1150
<s, cons>(q_gen_1108, q_gen_1127) -> q_gen_1151
<s, cons>(q_gen_1113, q_gen_1153) -> q_gen_1152
<s, cons>(q_gen_1108, q_gen_1111) -> q_gen_1153
<s, cons>(q_gen_1105, q_gen_1155) -> q_gen_1154
<s, cons>(q_gen_1113, q_gen_1138) -> q_gen_1155
<s, cons>(q_gen_1108, q_gen_1157) -> q_gen_1156
<s, cons>(q_gen_1105, q_gen_1158) -> q_gen_1157
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1158
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1159
<s, cons>(q_gen_1113, q_gen_1127) -> q_gen_1160
<s, cons>(q_gen_1113, q_gen_1151) -> q_gen_1161
<s, cons>(q_gen_1108, q_gen_1135) -> q_gen_1162
<s, cons>(q_gen_1136, q_gen_1151) -> q_gen_1163
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1164
<s, cons>(q_gen_1108, q_gen_1166) -> q_gen_1165
<s, cons>(q_gen_1136, q_gen_1103) -> q_gen_1166
<s, cons>(q_gen_1136, q_gen_1125) -> q_gen_1167
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004515 s (model generation: 0.004299,  model checking: 0.000216):

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

}

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

}
--
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.006749 s (model generation: 0.005277,  model checking: 0.001472):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105},
Q_f={q_gen_1103},
Delta=
{
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
}

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

}
--
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.005155 s (model generation: 0.004620,  model checking: 0.000535):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<s>(q_gen_1105) -> q_gen_1105
<z>() -> q_gen_1105
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
}

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

}
--
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.005661 s (model generation: 0.005448,  model checking: 0.000213):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<s>(q_gen_1105) -> q_gen_1105
<z>() -> q_gen_1105
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, nil>() -> q_gen_1103
}

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

}
--
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.007330 s (model generation: 0.005070,  model checking: 0.002260):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 5, which took 0.006194 s (model generation: 0.004539,  model checking: 0.001655):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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.007361 s (model generation: 0.006118,  model checking: 0.001243):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 6
(memberl([e, nil])) -> BOT -> 7
(memberl([i, l2])) -> memberl([i, l2]) -> 6
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 7, which took 0.005936 s (model generation: 0.005200,  model checking: 0.000736):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<s>(q_gen_1108) -> q_gen_1105
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 9
(memberl([e, nil])) -> BOT -> 7
(memberl([i, l2])) -> memberl([i, l2]) -> 7
}
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 8, which took 0.009432 s (model generation: 0.007634,  model checking: 0.001798):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 9
(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(z, cons(z, nil))
})

-------------------------------------------
Step 9, which took 0.008695 s (model generation: 0.006596,  model checking: 0.002099):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 10
(memberl([e, nil])) -> BOT -> 9
(memberl([i, l2])) -> memberl([i, l2]) -> 9
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> z  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 10, which took 0.007801 s (model generation: 0.006167,  model checking: 0.001634):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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)]) -> 11
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 11
(memberl([e, nil])) -> BOT -> 10
(memberl([i, l2])) -> memberl([i, l2]) -> 10
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 11, which took 0.007686 s (model generation: 0.006552,  model checking: 0.001134):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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)]) -> 11
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 14
(memberl([e, nil])) -> BOT -> 11
(memberl([i, l2])) -> memberl([i, l2]) -> 11
}
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 12, which took 0.010879 s (model generation: 0.008287,  model checking: 0.002592):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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)]) -> 14
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 14
(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 -> z  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 13, which took 0.009013 s (model generation: 0.007490,  model checking: 0.001523):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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)]) -> 14
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 17
(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 -> z  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 14, which took 0.016231 s (model generation: 0.009747,  model checking: 0.006484):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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)]) -> 15
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 17
(memberl([e, nil])) -> BOT -> 14
(memberl([i, l2])) -> memberl([i, l2]) -> 14
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.014715 s (model generation: 0.009492,  model checking: 0.005223):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 20
(memberl([e, nil])) -> BOT -> 15
(memberl([i, l2])) -> memberl([i, l2]) -> 15
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(z)  ;  h1 -> z  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.011072 s (model generation: 0.010820,  model checking: 0.000252):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<s, nil>(q_gen_1105) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1103
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 20
(memberl([e, nil])) -> BOT -> 18
(memberl([i, l2])) -> memberl([i, l2]) -> 16
}
Sat witness: Found: ((memberl([e, nil])) -> BOT, {
e -> s(z)
})

-------------------------------------------
Step 17, which took 0.011699 s (model generation: 0.008847,  model checking: 0.002852):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 20
(memberl([e, nil])) -> BOT -> 18
(memberl([i, l2])) -> memberl([i, l2]) -> 17
}
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(z, cons(s(z), cons(s(z), cons(s(z), nil))))
})

-------------------------------------------
Step 18, which took 0.016017 s (model generation: 0.014322,  model checking: 0.001695):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 20
(memberl([e, nil])) -> BOT -> 19
(memberl([i, l2])) -> memberl([i, l2]) -> 18
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(s(z)))  ;  t1 -> nil
})

-------------------------------------------
Step 19, which took 0.016250 s (model generation: 0.015569,  model checking: 0.000681):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, nil>(q_gen_1108) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 20
(memberl([e, nil])) -> BOT -> 22
(memberl([i, l2])) -> memberl([i, l2]) -> 19
}
Sat witness: Found: ((memberl([e, nil])) -> BOT, {
e -> s(s(z))
})

-------------------------------------------
Step 20, which took 0.017467 s (model generation: 0.015524,  model checking: 0.001943):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 20
(memberl([e, nil])) -> BOT -> 22
(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(z)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 21, which took 0.017474 s (model generation: 0.015672,  model checking: 0.001802):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1108
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 23
(memberl([e, nil])) -> BOT -> 22
(memberl([i, l2])) -> memberl([i, l2]) -> 21
}
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 22, which took 0.020644 s (model generation: 0.016597,  model checking: 0.004047):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1113) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
}

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

}
--
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]) -> 23
(memberl([e, nil])) -> BOT -> 22
(memberl([i, l2])) -> memberl([i, l2]) -> 22
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 23, which took 0.039540 s (model generation: 0.017013,  model checking: 0.022527):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1110, q_gen_1113},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1110) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1110) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1109
<s, cons>(q_gen_1113, q_gen_1110) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1110
<z, nil>() -> q_gen_1110
}

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

}
--
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 -> 23
(memberl([i, l2])) -> memberl([i, l2]) -> 23
}
Sat witness: Found: ((memberl([e, t1]) /\ not eq_nat([e, h1])) -> memberl([e, cons(h1, t1)]), {
e -> z  ;  h1 -> s(s(z))  ;  t1 -> cons(s(s(z)), cons(z, nil))
})

-------------------------------------------
Step 24, which took 0.050348 s (model generation: 0.019306,  model checking: 0.031042):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1110, q_gen_1113},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1110) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1110) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1109
<s, cons>(q_gen_1113, q_gen_1110) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1110
<z, nil>() -> q_gen_1110
}

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

}
--
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]) -> 26
(memberl([e, nil])) -> BOT -> 24
(memberl([i, l2])) -> memberl([i, l2]) -> 24
}
Sat witness: Found: ((memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]), {
e -> s(s(s(s(z))))  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(z, cons(z, cons(s(s(z)), nil))))
})

-------------------------------------------
Step 25, which took 12.297299 s (model generation: 0.065764,  model checking: 12.231535):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1110, q_gen_1113},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1110) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1109
<s, cons>(q_gen_1113, q_gen_1110) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1110) -> q_gen_1110
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1110
<z, nil>() -> q_gen_1110
}

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

}
--
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]) -> 26
(memberl([e, nil])) -> BOT -> 25
(memberl([i, l2])) -> memberl([i, l2]) -> 25
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 26, which took 4.091048 s (model generation: 0.035400,  model checking: 4.055648):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1116
<s, nil>(q_gen_1108) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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]) -> 26
(memberl([e, nil])) -> BOT -> 26
(memberl([i, l2])) -> memberl([i, l2]) -> 26
}
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(z), cons(z, nil))
})

-------------------------------------------
Step 27, which took 0.070052 s (model generation: 0.040088,  model checking: 0.029964):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1116) -> q_gen_1109
<s, nil>(q_gen_1105) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1116
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1116
<s, nil>(q_gen_1108) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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]) -> 29
(memberl([e, nil])) -> BOT -> 27
(memberl([i, l2])) -> memberl([i, l2]) -> 27
}
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 28, which took 0.072467 s (model generation: 0.041228,  model checking: 0.031239):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1116) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1116
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1116
<s, nil>(q_gen_1105) -> q_gen_1116
<s, nil>(q_gen_1108) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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 -> 28
(memberl([i, l2])) -> memberl([i, l2]) -> 28
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(z))  ;  t1 -> cons(s(z), cons(z, cons(z, nil)))
})

-------------------------------------------
Step 29, which took 0.747995 s (model generation: 0.046735,  model checking: 0.701260):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1116) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1116
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1116
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1116
<s, nil>(q_gen_1105) -> q_gen_1116
<s, nil>(q_gen_1108) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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 -> 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(s(z)))  ;  h1 -> s(z)  ;  t1 -> cons(z, cons(s(s(z)), cons(s(s(z)), nil)))
})

-------------------------------------------
Step 30, which took 0.883575 s (model generation: 0.068934,  model checking: 0.814641):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1113) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1116) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1116
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1116
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1116
<s, nil>(q_gen_1105) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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 -> 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 -> s(z)  ;  h1 -> z  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 31, which took 3.259811 s (model generation: 0.085991,  model checking: 3.173820):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1116) -> q_gen_1109
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1116
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1116
<s, nil>(q_gen_1105) -> q_gen_1116
<s, nil>(q_gen_1108) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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)]) -> 31
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 32
(memberl([e, nil])) -> BOT -> 31
(memberl([i, l2])) -> memberl([i, l2]) -> 31
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(z)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 32, which took 0.197709 s (model generation: 0.081433,  model checking: 0.116276):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1116},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1113) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1106) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1116) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1116
<s, cons>(q_gen_1105, q_gen_1116) -> q_gen_1116
<s, cons>(q_gen_1108, q_gen_1116) -> q_gen_1116
<s, nil>(q_gen_1105) -> q_gen_1116
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1116
}

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

}
--
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)]) -> 34
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 32
(memberl([e, nil])) -> BOT -> 32
(memberl([i, l2])) -> memberl([i, l2]) -> 32
}
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 33, which took 0.099495 s (model generation: 0.068642,  model checking: 0.030853):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1124},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1124) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1103) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1124) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1124
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1124
<s, cons>(q_gen_1108, q_gen_1124) -> q_gen_1124
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1124
<s, nil>(q_gen_1105) -> q_gen_1124
<s, nil>(q_gen_1108) -> q_gen_1124
}

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

}
--
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)]) -> 34
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 35
(memberl([e, nil])) -> BOT -> 33
(memberl([i, l2])) -> memberl([i, l2]) -> 33
}
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), nil)
})

-------------------------------------------
Step 34, which took 0.174488 s (model generation: 0.084133,  model checking: 0.090355):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1124},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s>(q_gen_1113) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1124) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1124) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1124) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1124
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1124
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1124
<s, nil>(q_gen_1105) -> q_gen_1124
<s, nil>(q_gen_1108) -> q_gen_1124
}

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

}
--
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)]) -> 34
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 35
(memberl([e, nil])) -> BOT -> 34
(memberl([i, l2])) -> memberl([i, l2]) -> 34
}
Sat witness: Found: (() -> memberl([h1, cons(h1, t1)]), {
h1 -> s(s(s(z)))  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 35, which took 2.750657 s (model generation: 0.080902,  model checking: 2.669755):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1113, q_gen_1124},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1113) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1124) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1106) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<s, cons>(q_gen_1113, q_gen_1124) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1124) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1109
<z, nil>() -> q_gen_1109
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1124
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1124
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1124
<s, nil>(q_gen_1105) -> q_gen_1124
}

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

}
--
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)]) -> 37
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 35
(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 1.334583 s (model generation: 0.106158,  model checking: 1.228425):

Model:
|_
{
memberl -> 
{{{
Q={q_gen_1103, q_gen_1104, q_gen_1105, q_gen_1106, q_gen_1107, q_gen_1108, q_gen_1109, q_gen_1110, q_gen_1113, q_gen_1125},
Q_f={q_gen_1103, q_gen_1106},
Delta=
{
<cons>(q_gen_1108, q_gen_1104) -> q_gen_1104
<nil>() -> q_gen_1104
<s>(q_gen_1113) -> q_gen_1105
<z>() -> q_gen_1105
<cons>(q_gen_1105, q_gen_1104) -> q_gen_1107
<cons>(q_gen_1105, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1108, q_gen_1107) -> q_gen_1107
<cons>(q_gen_1113, q_gen_1107) -> q_gen_1107
<s>(q_gen_1105) -> q_gen_1108
<s>(q_gen_1108) -> q_gen_1113
<s, cons>(q_gen_1105, q_gen_1109) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1103) -> q_gen_1103
<s, cons>(q_gen_1108, q_gen_1110) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1106) -> q_gen_1103
<s, cons>(q_gen_1113, q_gen_1109) -> q_gen_1103
<z, cons>(q_gen_1105, q_gen_1104) -> q_gen_1103
<s, cons>(q_gen_1105, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1106) -> q_gen_1106
<s, cons>(q_gen_1108, q_gen_1109) -> q_gen_1106
<z, cons>(q_gen_1105, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1108, q_gen_1107) -> q_gen_1106
<z, cons>(q_gen_1113, q_gen_1107) -> q_gen_1106
<s, cons>(q_gen_1105, q_gen_1103) -> q_gen_1109
<s, cons>(q_gen_1108, q_gen_1125) -> q_gen_1109
<s, nil>(q_gen_1108) -> q_gen_1109
<z, cons>(q_gen_1108, q_gen_1104) -> q_gen_1109
<s, cons>(q_gen_1113, q_gen_1125) -> q_gen_1110
<z, cons>(q_gen_1113, q_gen_1104) -> q_gen_1110
<z, nil>() -> q_gen_1110
<s, cons>(q_gen_1105, q_gen_1110) -> q_gen_1125
<s, cons>(q_gen_1105, q_gen_1125) -> q_gen_1125
<s, cons>(q_gen_1113, q_gen_1110) -> q_gen_1125
<s, nil>(q_gen_1105) -> q_gen_1125
}

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

}
--
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)]) -> 37
(memberl([e, cons(h1, t1)]) /\ not eq_nat([e, h1])) -> memberl([e, t1]) -> 38
(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(s(z))  ;  h1 -> s(z)  ;  t1 -> cons(s(s(s(z))), cons(z, nil))
})

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