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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(elem, P:
{() -> elem([h1, cons(h1, t1)])
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)])
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1])
(elem([e, nil])) -> BOT}
)
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)])}
(append([_sj, _tj, _uj]) /\ append([_sj, _tj, _vj])) -> eq_eltlist([_uj, _vj])
)
}

properties:
{(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> elem([h1, cons(h1, t1)]) -> 0
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 0
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 0
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 0
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 0
(elem([e, nil])) -> BOT -> 0
}


Solving took 30.349821 seconds.
Proved
Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550, q_gen_2559},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons>(q_gen_2477, q_gen_2559) -> q_gen_2559
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2559
<cons, cons>(q_gen_2548, q_gen_2559) -> q_gen_2559
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2559) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2559) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, cons, cons>(q_gen_2491, q_gen_2550) -> q_gen_2550
<cons, nil, cons>(q_gen_2477, q_gen_2559) -> q_gen_2550
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008725 s (model generation: 0.008425,  model checking: 0.000300):

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

}

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

}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 1
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 1
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 1
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 1
(elem([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 1, which took 0.012092 s (model generation: 0.011880,  model checking: 0.000212):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 1
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 1
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 1
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 1
(elem([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.010702 s (model generation: 0.010351,  model checking: 0.000351):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 1
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 1
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 2
(elem([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 3, which took 0.008526 s (model generation: 0.008357,  model checking: 0.000169):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<a>() -> q_gen_2470
<b>() -> q_gen_2470
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 1
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 4
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 2
(elem([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.009678 s (model generation: 0.009526,  model checking: 0.000152):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477},
Q_f={q_gen_2471},
Delta=
{
<nil, nil>() -> q_gen_2476
<b, b>() -> q_gen_2477
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<a>() -> q_gen_2470
<b>() -> q_gen_2470
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 2
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 4
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 3
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.009065 s (model generation: 0.008989,  model checking: 0.000076):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477},
Q_f={q_gen_2471},
Delta=
{
<nil, nil>() -> q_gen_2476
<b, b>() -> q_gen_2477
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<a>() -> q_gen_2470
<b>() -> q_gen_2470
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, nil>() -> q_gen_2468
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> elem([h1, cons(h1, t1)]) -> 3
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 3
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 4
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((elem([e, nil])) -> BOT, {
e -> b
})

-------------------------------------------
Step 6, which took 0.010185 s (model generation: 0.009713,  model checking: 0.000472):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477},
Q_f={q_gen_2471},
Delta=
{
<nil, nil>() -> q_gen_2476
<b, b>() -> q_gen_2477
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> elem([h1, cons(h1, t1)]) -> 6
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 4
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 4
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 6
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.009252 s (model generation: 0.008939,  model checking: 0.000313):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477},
Q_f={q_gen_2471},
Delta=
{
<nil, nil>() -> q_gen_2476
<b, b>() -> q_gen_2477
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> elem([h1, cons(h1, t1)]) -> 6
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 4
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 4
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 4
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 6
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 8, which took 0.010933 s (model generation: 0.010482,  model checking: 0.000451):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477},
Q_f={q_gen_2471},
Delta=
{
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> elem([h1, cons(h1, t1)]) -> 6
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 4
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 4
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 9, which took 0.014260 s (model generation: 0.012738,  model checking: 0.001522):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477},
Q_f={q_gen_2471},
Delta=
{
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> elem([h1, cons(h1, t1)]) -> 6
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 4
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 7
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.014996 s (model generation: 0.013011,  model checking: 0.001985):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> elem([h1, cons(h1, t1)]) -> 6
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 7
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 7
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 5
(elem([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(b, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.016720 s (model generation: 0.015293,  model checking: 0.001427):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 7
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 7
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 7
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 6
(elem([e, nil])) -> BOT -> 7
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 12, which took 0.014484 s (model generation: 0.012361,  model checking: 0.002123):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 7
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 7
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 7
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.014486 s (model generation: 0.014233,  model checking: 0.000253):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 7
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 7
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 10
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 14, which took 0.015053 s (model generation: 0.013849,  model checking: 0.001204):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 7
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 10
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 10
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.017388 s (model generation: 0.014920,  model checking: 0.002468):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> elem([h1, cons(h1, t1)]) -> 9
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 10
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 10
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 10
(elem([e, nil])) -> BOT -> 8
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 16, which took 0.017071 s (model generation: 0.016241,  model checking: 0.000830):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 10
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 10
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 10
(elem([e, nil])) -> BOT -> 9
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 17, which took 0.017649 s (model generation: 0.016695,  model checking: 0.000954):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 10
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 10
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 13
(elem([e, nil])) -> BOT -> 10
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 18, which took 0.018152 s (model generation: 0.017534,  model checking: 0.000618):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, nil>() -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 10
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 10
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 10
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((elem([e, nil])) -> BOT, {
e -> a
})

-------------------------------------------
Step 19, which took 0.019025 s (model generation: 0.017859,  model checking: 0.001166):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 10
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 10
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 20, which took 0.020303 s (model generation: 0.018980,  model checking: 0.001323):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 10
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 13
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.020925 s (model generation: 0.019090,  model checking: 0.001835):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> elem([h1, cons(h1, t1)]) -> 12
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 13
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 13
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(a, nil))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 22, which took 0.022334 s (model generation: 0.021390,  model checking: 0.000944):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> elem([h1, cons(h1, t1)]) -> 15
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 13
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 13
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 13
(elem([e, nil])) -> BOT -> 13
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 23, which took 0.024147 s (model generation: 0.023083,  model checking: 0.001064):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> elem([h1, cons(h1, t1)]) -> 15
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 13
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 13
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 13
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.024411 s (model generation: 0.021520,  model checking: 0.002891):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> elem([h1, cons(h1, t1)]) -> 15
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 13
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 13
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 25, which took 0.025817 s (model generation: 0.024303,  model checking: 0.001514):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> elem([h1, cons(h1, t1)]) -> 15
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 13
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 16
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.029321 s (model generation: 0.025227,  model checking: 0.004094):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> elem([h1, cons(h1, t1)]) -> 15
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 16
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 16
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 16
(elem([e, nil])) -> BOT -> 14
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> cons(b, cons(b, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 27, which took 0.032041 s (model generation: 0.031119,  model checking: 0.000922):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> elem([h1, cons(h1, t1)]) -> 18
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 16
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 16
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 16
(elem([e, nil])) -> BOT -> 15
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.035201 s (model generation: 0.031629,  model checking: 0.003572):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> elem([h1, cons(h1, t1)]) -> 18
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 16
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 16
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 16
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 19
(elem([e, nil])) -> BOT -> 16
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, cons(b, nil)))
})

-------------------------------------------
Step 29, which took 0.036702 s (model generation: 0.033861,  model checking: 0.002841):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> elem([h1, cons(h1, t1)]) -> 18
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 16
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 16
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 19
(elem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 30, which took 0.037755 s (model generation: 0.036521,  model checking: 0.001234):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> elem([h1, cons(h1, t1)]) -> 18
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 16
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 19
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 19
(elem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(a, nil)  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 31, which took 0.042760 s (model generation: 0.037554,  model checking: 0.005206):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> elem([h1, cons(h1, t1)]) -> 18
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 19
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 19
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 19
(elem([e, nil])) -> BOT -> 17
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(b, cons(a, cons(b, nil))))  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> cons(b, cons(b, cons(a, cons(b, nil))))
})

-------------------------------------------
Step 32, which took 0.045018 s (model generation: 0.044366,  model checking: 0.000652):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> elem([h1, cons(h1, t1)]) -> 21
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 19
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 19
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 19
(elem([e, nil])) -> BOT -> 18
}
Sat witness: Found: (() -> elem([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 33, which took 0.048130 s (model generation: 0.046956,  model checking: 0.001174):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2473
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> elem([h1, cons(h1, t1)]) -> 21
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 19
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 19
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 19
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 22
(elem([e, nil])) -> BOT -> 19
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 34, which took 0.052074 s (model generation: 0.049725,  model checking: 0.002349):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> elem([h1, cons(h1, t1)]) -> 21
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 19
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 19
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 22
(elem([e, nil])) -> BOT -> 20
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 35, which took 0.054038 s (model generation: 0.052853,  model checking: 0.001185):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> elem([h1, cons(h1, t1)]) -> 21
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 19
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 22
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 22
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 22
(elem([e, nil])) -> BOT -> 20
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 36, which took 0.067191 s (model generation: 0.055794,  model checking: 0.011397):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> elem([h1, cons(h1, t1)]) -> 22
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 20
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 22
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23
(elem([e, nil])) -> BOT -> 21
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 37, which took 0.066814 s (model generation: 0.060063,  model checking: 0.006751):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
() -> elem([h1, cons(h1, t1)]) -> 22
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 23
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 22
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23
(elem([e, nil])) -> BOT -> 21
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(b, cons(a, cons(b, nil))))  ;  i -> a  ;  l1 -> cons(b, cons(b, cons(a, nil)))  ;  l2 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 38, which took 0.081161 s (model generation: 0.077387,  model checking: 0.003774):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21
() -> elem([h1, cons(h1, t1)]) -> 22
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 23
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 25
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 23
(elem([e, nil])) -> BOT -> 22
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 39, which took 0.083066 s (model generation: 0.081805,  model checking: 0.001261):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> elem([h1, cons(h1, t1)]) -> 23
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 23
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 25
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26
(elem([e, nil])) -> BOT -> 23
}
Sat witness: Found: ((elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]), {
e -> a  ;  h1 -> b  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 40, which took 0.087228 s (model generation: 0.084306,  model checking: 0.002922):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> elem([h1, cons(h1, t1)]) -> 23
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 26
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 25
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26
(elem([e, nil])) -> BOT -> 24
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(a, nil)  ;  i -> b  ;  l1 -> cons(b, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 41, which took 0.086665 s (model generation: 0.086110,  model checking: 0.000555):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2483, q_gen_2486, q_gen_2489, q_gen_2490, q_gen_2491},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<cons, cons>(q_gen_2483, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<b, b>() -> q_gen_2477
<a, a>() -> q_gen_2483
<b, a>() -> q_gen_2483
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, cons, cons>(q_gen_2491, q_gen_2486) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2483, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<cons, nil, cons>(q_gen_2483, q_gen_2476) -> q_gen_2486
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2486
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2486
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2469
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> elem([h1, cons(h1, t1)]) -> 24
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 26
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 25
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 25
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26
(elem([e, nil])) -> BOT -> 24
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 42, which took 0.086974 s (model generation: 0.084505,  model checking: 0.002469):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2483, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2544},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<cons, cons>(q_gen_2483, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<b, b>() -> q_gen_2477
<a, a>() -> q_gen_2483
<b, a>() -> q_gen_2483
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, cons, cons>(q_gen_2491, q_gen_2544) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2483, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2483, q_gen_2476) -> q_gen_2544
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> elem([h1, cons(h1, t1)]) -> 25
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 26
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 28
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 26
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 26
(elem([e, nil])) -> BOT -> 25
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 43, which took 0.115508 s (model generation: 0.089503,  model checking: 0.026005):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<b, a>() -> q_gen_2548
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> elem([h1, cons(h1, t1)]) -> 26
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 27
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 31
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 27
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 27
(elem([e, nil])) -> BOT -> 26
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 44, which took 0.139120 s (model generation: 0.114884,  model checking: 0.024236):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> elem([h1, cons(h1, t1)]) -> 27
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 28
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 34
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 28
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 28
(elem([e, nil])) -> BOT -> 27
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, cons(a, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(b, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 45, which took 0.128732 s (model generation: 0.120123,  model checking: 0.008609):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> elem([h1, cons(h1, t1)]) -> 28
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 31
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 34
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 29
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 29
(elem([e, nil])) -> BOT -> 28
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(b, cons(b, nil))  ;  i -> a  ;  l1 -> cons(b, cons(a, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 46, which took 0.149070 s (model generation: 0.135720,  model checking: 0.013350):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2482, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2482) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2482
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2482
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, cons, cons>(q_gen_2491, q_gen_2550) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2482) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2477, q_gen_2482) -> q_gen_2550
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
<nil, cons, cons>(q_gen_2548, q_gen_2482) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
() -> elem([h1, cons(h1, t1)]) -> 29
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 31
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 34
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 32
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 30
(elem([e, nil])) -> BOT -> 29
}
Sat witness: Found: ((elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]), {
e -> b  ;  h1 -> a  ;  t1 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 47, which took 0.146763 s (model generation: 0.138929,  model checking: 0.007834):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2488, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2498, q_gen_2548},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<cons, cons>(q_gen_2548, q_gen_2498) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2498
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2498
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons, cons>(q_gen_2491, q_gen_2488) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2488
<cons, nil, cons>(q_gen_2477, q_gen_2498) -> q_gen_2488
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2488
<nil, cons, cons>(q_gen_2477, q_gen_2498) -> q_gen_2488
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2488
<nil, cons, cons>(q_gen_2548, q_gen_2498) -> q_gen_2488
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2488
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> elem([h1, cons(h1, t1)]) -> 30
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 34
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 34
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 32
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 31
(elem([e, nil])) -> BOT -> 30
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))  ;  i -> b  ;  l1 -> cons(a, cons(a, cons(b, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 48, which took 0.143479 s (model generation: 0.139572,  model checking: 0.003907):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2482, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2547, q_gen_2548},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2482
<cons, cons>(q_gen_2477, q_gen_2482) -> q_gen_2482
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2482
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, cons, cons>(q_gen_2491, q_gen_2547) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2482) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2477, q_gen_2482) -> q_gen_2547
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2547
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2547
<nil, cons, cons>(q_gen_2548, q_gen_2482) -> q_gen_2547
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> elem([h1, cons(h1, t1)]) -> 31
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 34
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 37
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 33
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 32
(elem([e, nil])) -> BOT -> 31
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 49, which took 0.230638 s (model generation: 0.219418,  model checking: 0.011220):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2547, q_gen_2548, q_gen_2559},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons>(q_gen_2477, q_gen_2559) -> q_gen_2559
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2559
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, cons, cons>(q_gen_2491, q_gen_2547) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, nil, cons>(q_gen_2477, q_gen_2559) -> q_gen_2547
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2547
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2547
<nil, cons, cons>(q_gen_2548, q_gen_2559) -> q_gen_2547
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
() -> elem([h1, cons(h1, t1)]) -> 32
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 37
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 37
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 34
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 33
(elem([e, nil])) -> BOT -> 32
}
Sat witness: Found: ((append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]), {
_wj -> cons(a, cons(a, cons(a, nil)))  ;  i -> b  ;  l1 -> cons(a, cons(b, cons(a, nil)))  ;  l2 -> cons(b, nil)
})

-------------------------------------------
Step 50, which took 0.231943 s (model generation: 0.206161,  model checking: 0.025782):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550, q_gen_2559},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons>(q_gen_2477, q_gen_2559) -> q_gen_2559
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2559
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2559) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, cons, cons>(q_gen_2491, q_gen_2550) -> q_gen_2550
<cons, nil, cons>(q_gen_2477, q_gen_2559) -> q_gen_2550
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
() -> elem([h1, cons(h1, t1)]) -> 33
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 37
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 40
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 35
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 34
(elem([e, nil])) -> BOT -> 33
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 51, which took 0.243421 s (model generation: 0.198729,  model checking: 0.044692):

Model:
|_
{
append -> 
{{{
Q={q_gen_2471, q_gen_2476, q_gen_2477, q_gen_2489, q_gen_2490, q_gen_2491, q_gen_2548, q_gen_2550, q_gen_2559},
Q_f={q_gen_2471},
Delta=
{
<cons>(q_gen_2490, q_gen_2489) -> q_gen_2489
<nil>() -> q_gen_2489
<a>() -> q_gen_2490
<b>() -> q_gen_2490
<cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2476
<nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2476
<nil, nil>() -> q_gen_2476
<a, a>() -> q_gen_2477
<b, b>() -> q_gen_2477
<a, b>() -> q_gen_2548
<b, a>() -> q_gen_2548
<cons, cons>(q_gen_2477, q_gen_2559) -> q_gen_2559
<cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2559
<cons, cons, cons>(q_gen_2491, q_gen_2471) -> q_gen_2471
<cons, nil, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2477, q_gen_2559) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2476) -> q_gen_2471
<nil, cons, cons>(q_gen_2548, q_gen_2559) -> q_gen_2471
<nil, nil, cons>(q_gen_2490, q_gen_2489) -> q_gen_2471
<nil, nil, nil>() -> q_gen_2471
<a, a, a>() -> q_gen_2491
<a, b, a>() -> q_gen_2491
<b, a, b>() -> q_gen_2491
<b, b, b>() -> q_gen_2491
<cons, cons, cons>(q_gen_2491, q_gen_2550) -> q_gen_2550
<cons, nil, cons>(q_gen_2477, q_gen_2559) -> q_gen_2550
<cons, nil, cons>(q_gen_2548, q_gen_2476) -> q_gen_2550
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  elem -> 
{{{
Q={q_gen_2468, q_gen_2469, q_gen_2470, q_gen_2473, q_gen_2474, q_gen_2478, q_gen_2485, q_gen_2495},
Q_f={q_gen_2468},
Delta=
{
<nil>() -> q_gen_2469
<b>() -> q_gen_2470
<cons>(q_gen_2470, q_gen_2469) -> q_gen_2473
<cons>(q_gen_2470, q_gen_2473) -> q_gen_2473
<a>() -> q_gen_2474
<cons>(q_gen_2470, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2470, q_gen_2495) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2473) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2485) -> q_gen_2485
<cons>(q_gen_2474, q_gen_2469) -> q_gen_2495
<cons>(q_gen_2474, q_gen_2495) -> q_gen_2495
<a, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2469) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2474, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2469) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2485) -> q_gen_2468
<b, cons>(q_gen_2470, q_gen_2495) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2473) -> q_gen_2468
<b, cons>(q_gen_2474, q_gen_2485) -> q_gen_2468
<a, cons>(q_gen_2470, q_gen_2469) -> q_gen_2478
<a, cons>(q_gen_2470, q_gen_2473) -> q_gen_2478
<a, nil>() -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2469) -> q_gen_2478
<b, cons>(q_gen_2474, q_gen_2495) -> q_gen_2478
<b, nil>() -> q_gen_2478
}

Datatype: <elt, eltlist>
Convolution form: left
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 34
() -> elem([h1, cons(h1, t1)]) -> 34
(append([l1, l2, _wj]) /\ elem([i, l1])) -> elem([i, _wj]) -> 38
(append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]) -> 43
(elem([e, t1]) /\ not eq_elt([e, h1])) -> elem([e, cons(h1, t1)]) -> 36
(elem([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> elem([e, t1]) -> 35
(elem([e, nil])) -> BOT -> 34
}
Sat witness: Found: ((append([t1, l2, _rj])) -> append([cons(h1, t1), l2, cons(h1, _rj)]), {
_rj -> cons(a, cons(b, cons(b, cons(a, cons(b, nil)))))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, cons(a, cons(b, nil)))))  ;  t1 -> nil
})

Total time: 30.349821
Reason for stopping: Proved