Solving ../../benchmarks/false/timbuk_reverseBUGimplies.smt2...

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, nil])
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)])}
(append([_aka, _bka, _cka]) /\ append([_aka, _bka, _dka])) -> eq_eltlist([_cka, _dka])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka])}
(reverse([_gka, _hka]) /\ reverse([_gka, _ika])) -> eq_eltlist([_hka, _ika])
)
(member, P:
{() -> member([h1, cons(h1, t1)])
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)])
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1])
(member([e, nil])) -> BOT}
)
}

properties:
{(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka])}


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

Clause system for inference is:

{
() -> append([nil, l2, nil]) -> 0
() -> member([h1, cons(h1, t1)]) -> 0
() -> reverse([nil, nil]) -> 0
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 0
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 0
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 0
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 0
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 0
(member([e, nil])) -> BOT -> 0
}


Solving took 0.294967 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.016808 s (model generation: 0.016118,  model checking: 0.000690):

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

}

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

}

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 0
() -> member([h1, cons(h1, t1)]) -> 0
() -> reverse([nil, nil]) -> 3
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 1
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 1
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 1
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 1
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 1
(member([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> reverse([nil, nil]), {

})

-------------------------------------------
Step 1, which took 0.016888 s (model generation: 0.016706,  model checking: 0.000182):

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

}

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

}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 0
() -> member([h1, cons(h1, t1)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 1
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 1
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 1
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 1
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 1
(member([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> member([h1, cons(h1, t1)]), {
h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.017414 s (model generation: 0.017060,  model checking: 0.000354):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 3
() -> member([h1, cons(h1, t1)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 1
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 1
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 1
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 1
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 1
(member([e, nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, nil]), {
l2 -> nil
})

-------------------------------------------
Step 3, which took 0.018610 s (model generation: 0.017241,  model checking: 0.001369):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

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

-------------------------------------------
Step 4, which took 0.018748 s (model generation: 0.018155,  model checking: 0.000593):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955},
Q_f={q_gen_8953},
Delta=
{
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8954
<nil>() -> q_gen_8954
<a>() -> q_gen_8955
<b>() -> q_gen_8955
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 3
() -> member([h1, cons(h1, t1)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 1
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 4
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 2
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 4
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 2
(member([e, nil])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]), {
_zja -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.019108 s (model generation: 0.018772,  model checking: 0.000336):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962},
Q_f={q_gen_8956},
Delta=
{
<nil, nil>() -> q_gen_8961
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955},
Q_f={q_gen_8953},
Delta=
{
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8954
<nil>() -> q_gen_8954
<a>() -> q_gen_8955
<b>() -> q_gen_8955
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

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

-------------------------------------------
Step 6, which took 0.020462 s (model generation: 0.020185,  model checking: 0.000277):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962},
Q_f={q_gen_8956},
Delta=
{
<nil, nil>() -> q_gen_8961
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955},
Q_f={q_gen_8953},
Delta=
{
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8954
<nil>() -> q_gen_8954
<a>() -> q_gen_8955
<b>() -> q_gen_8955
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, nil>() -> q_gen_8953
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 3
() -> member([h1, cons(h1, t1)]) -> 3
() -> reverse([nil, nil]) -> 3
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 3
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 4
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 3
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 4
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 5
(member([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((member([e, nil])) -> BOT, {
e -> b
})

-------------------------------------------
Step 7, which took 0.022252 s (model generation: 0.021314,  model checking: 0.000938):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962},
Q_f={q_gen_8956},
Delta=
{
<nil, nil>() -> q_gen_8961
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955, q_gen_8958, q_gen_8959, q_gen_8963},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8958
<a>() -> q_gen_8959
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8958) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8954) -> q_gen_8963
<b, nil>() -> q_gen_8963
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 3
() -> member([h1, cons(h1, t1)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 4
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 4
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 4
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 4
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 5
(member([e, nil])) -> BOT -> 6
}
Sat witness: Found: (() -> member([h1, cons(h1, t1)]), {
h1 -> a  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.021914 s (model generation: 0.021452,  model checking: 0.000462):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962},
Q_f={q_gen_8956},
Delta=
{
<nil, nil>() -> q_gen_8961
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955, q_gen_8958, q_gen_8959, q_gen_8963},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8958
<a>() -> q_gen_8959
<a, cons>(q_gen_8959, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8958) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8954) -> q_gen_8963
<b, nil>() -> q_gen_8963
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 6
() -> member([h1, cons(h1, t1)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 4
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 4
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 4
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 4
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 5
(member([e, nil])) -> BOT -> 6
}
Sat witness: Found: (() -> append([nil, l2, nil]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 9, which took 0.024221 s (model generation: 0.022877,  model checking: 0.001344):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962, q_gen_8967, q_gen_8968},
Q_f={q_gen_8956},
Delta=
{
<nil>() -> q_gen_8967
<b>() -> q_gen_8968
<nil, nil>() -> q_gen_8961
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, cons, nil>(q_gen_8968, q_gen_8967) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955, q_gen_8958, q_gen_8959, q_gen_8963},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8958
<a>() -> q_gen_8959
<a, cons>(q_gen_8959, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8958) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8954) -> q_gen_8963
<b, nil>() -> q_gen_8963
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

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

-------------------------------------------
Step 10, which took 0.024206 s (model generation: 0.023121,  model checking: 0.001085):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962, q_gen_8967, q_gen_8968},
Q_f={q_gen_8956},
Delta=
{
<nil>() -> q_gen_8967
<b>() -> q_gen_8968
<nil, nil>() -> q_gen_8961
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, cons, nil>(q_gen_8968, q_gen_8967) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955, q_gen_8958, q_gen_8959, q_gen_8963},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8958
<cons>(q_gen_8959, q_gen_8958) -> q_gen_8958
<a>() -> q_gen_8959
<a, cons>(q_gen_8959, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8958) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8954) -> q_gen_8963
<b, nil>() -> q_gen_8963
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 6
() -> member([h1, cons(h1, t1)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 4
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 7
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 5
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 7
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 5
(member([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]), {
_zja -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.023896 s (model generation: 0.023654,  model checking: 0.000242):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962, q_gen_8967, q_gen_8968},
Q_f={q_gen_8956},
Delta=
{
<nil>() -> q_gen_8967
<b>() -> q_gen_8968
<nil, nil>() -> q_gen_8961
<a, a>() -> q_gen_8962
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, cons, nil>(q_gen_8968, q_gen_8967) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955, q_gen_8958, q_gen_8959, q_gen_8963},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8958
<cons>(q_gen_8959, q_gen_8958) -> q_gen_8958
<a>() -> q_gen_8959
<a, cons>(q_gen_8959, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8958) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8954) -> q_gen_8963
<b, nil>() -> q_gen_8963
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952},
Q_f={q_gen_8952},
Delta=
{
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 6
() -> member([h1, cons(h1, t1)]) -> 6
() -> reverse([nil, nil]) -> 4
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 7
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 7
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 5
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 7
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 5
(member([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]), {
_eka -> nil  ;  _fka -> nil  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.026825 s (model generation: 0.024229,  model checking: 0.002596):

Model:
|_
{
append -> 
{{{
Q={q_gen_8956, q_gen_8961, q_gen_8962, q_gen_8967, q_gen_8968},
Q_f={q_gen_8956},
Delta=
{
<nil>() -> q_gen_8967
<b>() -> q_gen_8968
<nil, nil>() -> q_gen_8961
<a, a>() -> q_gen_8962
<b, b>() -> q_gen_8962
<cons, nil, cons>(q_gen_8962, q_gen_8961) -> q_gen_8956
<nil, cons, nil>(q_gen_8968, q_gen_8967) -> q_gen_8956
<nil, nil, nil>() -> q_gen_8956
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: left
}}}
  ;  member -> 
{{{
Q={q_gen_8953, q_gen_8954, q_gen_8955, q_gen_8958, q_gen_8959, q_gen_8963},
Q_f={q_gen_8953},
Delta=
{
<nil>() -> q_gen_8954
<b>() -> q_gen_8955
<cons>(q_gen_8955, q_gen_8954) -> q_gen_8958
<cons>(q_gen_8959, q_gen_8958) -> q_gen_8958
<a>() -> q_gen_8959
<a, cons>(q_gen_8959, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8955, q_gen_8954) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8958) -> q_gen_8953
<b, cons>(q_gen_8959, q_gen_8954) -> q_gen_8963
<b, nil>() -> q_gen_8963
}

Datatype: <elt, eltlist>
Convolution form: left
}}}
  ;  reverse -> 
{{{
Q={q_gen_8952, q_gen_8974, q_gen_8975},
Q_f={q_gen_8952},
Delta=
{
<nil>() -> q_gen_8974
<b>() -> q_gen_8975
<cons, nil>(q_gen_8975, q_gen_8974) -> q_gen_8952
<nil, nil>() -> q_gen_8952
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, nil]) -> 6
() -> member([h1, cons(h1, t1)]) -> 6
() -> reverse([nil, nil]) -> 5
(append([_eka, cons(h1, nil), _fka]) /\ reverse([t1, _eka])) -> reverse([cons(h1, t1), _fka]) -> 7
(append([t1, l2, _zja])) -> append([cons(h1, t1), l2, cons(h1, _zja)]) -> 7
(member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]) -> 8
(member([e, t1]) /\ not eq_elt([e, h1])) -> member([e, cons(h1, t1)]) -> 7
(member([e, cons(h1, t1)]) /\ not eq_elt([e, h1])) -> member([e, t1]) -> 6
(member([e, nil])) -> BOT -> 6
}
Sat witness: Found: ((member([e, l1]) /\ reverse([l1, _jka])) -> member([e, _jka]), {
_jka -> nil  ;  e -> b  ;  l1 -> cons(b, nil)
})

Total time: 0.294967
Reason for stopping: Disproved