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

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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, nil])
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)])}
(append([_ila, _jla, _kla]) /\ append([_ila, _jla, _lla])) -> eq_eltlist([_kla, _lla])
)
(reverse, F:
{() -> reverse([nil, nil])
(append([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla])}
(reverse([_ola, _pla]) /\ reverse([_ola, _qla])) -> eq_eltlist([_pla, _qla])
)
(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, _rla])) -> member([e, _rla])}


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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 0
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 0
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.178735 seconds.
Disproved
-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010399 s (model generation: 0.009735,  model checking: 0.000664):

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

}

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

}

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

}

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 1
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 1
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.010806 s (model generation: 0.009952,  model checking: 0.000854):

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

}

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

}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 1
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 1
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.010740 s (model generation: 0.010466,  model checking: 0.000274):

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

}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 1
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 1
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.011073 s (model generation: 0.010422,  model checking: 0.000651):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 1
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 1
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.011853 s (model generation: 0.011038,  model checking: 0.000815):

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

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820},
Q_f={q_gen_6818},
Delta=
{
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6819
<nil>() -> q_gen_6819
<a>() -> q_gen_6820
<b>() -> q_gen_6820
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 1
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 4
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]), {
_hla -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.011632 s (model generation: 0.011295,  model checking: 0.000337):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827},
Q_f={q_gen_6821},
Delta=
{
<nil, nil>() -> q_gen_6826
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820},
Q_f={q_gen_6818},
Delta=
{
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6819
<nil>() -> q_gen_6819
<a>() -> q_gen_6820
<b>() -> q_gen_6820
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 2
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 4
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.012171 s (model generation: 0.011853,  model checking: 0.000318):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827},
Q_f={q_gen_6821},
Delta=
{
<nil, nil>() -> q_gen_6826
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820},
Q_f={q_gen_6818},
Delta=
{
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6819
<nil>() -> q_gen_6819
<a>() -> q_gen_6820
<b>() -> q_gen_6820
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, nil>() -> q_gen_6818
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 3
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 4
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.013137 s (model generation: 0.012004,  model checking: 0.001133):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827},
Q_f={q_gen_6821},
Delta=
{
<nil, nil>() -> q_gen_6826
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6823, q_gen_6824, q_gen_6828},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6823
<a>() -> q_gen_6824
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6823) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6819) -> q_gen_6828
<b, nil>() -> q_gen_6828
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 4
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 4
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.013024 s (model generation: 0.012487,  model checking: 0.000537):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827},
Q_f={q_gen_6821},
Delta=
{
<nil, nil>() -> q_gen_6826
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6823, q_gen_6824, q_gen_6828},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6823
<a>() -> q_gen_6824
<a, cons>(q_gen_6824, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6823) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6819) -> q_gen_6828
<b, nil>() -> q_gen_6828
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 4
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 4
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.014723 s (model generation: 0.013485,  model checking: 0.001238):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827, q_gen_6832, q_gen_6833},
Q_f={q_gen_6821},
Delta=
{
<nil>() -> q_gen_6832
<b>() -> q_gen_6833
<nil, nil>() -> q_gen_6826
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, cons, nil>(q_gen_6833, q_gen_6832) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6823, q_gen_6824, q_gen_6828},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6823
<a>() -> q_gen_6824
<a, cons>(q_gen_6824, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6823) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6819) -> q_gen_6828
<b, nil>() -> q_gen_6828
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 4
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 4
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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.014744 s (model generation: 0.013742,  model checking: 0.001002):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827, q_gen_6832, q_gen_6833},
Q_f={q_gen_6821},
Delta=
{
<nil>() -> q_gen_6832
<b>() -> q_gen_6833
<nil, nil>() -> q_gen_6826
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, cons, nil>(q_gen_6833, q_gen_6832) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6823, q_gen_6824, q_gen_6828},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6823
<cons>(q_gen_6824, q_gen_6823) -> q_gen_6823
<a>() -> q_gen_6824
<a, cons>(q_gen_6824, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6823) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6819) -> q_gen_6828
<b, nil>() -> q_gen_6828
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 4
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 7
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]), {
_hla -> nil  ;  h1 -> a  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.014260 s (model generation: 0.014041,  model checking: 0.000219):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827, q_gen_6832, q_gen_6833},
Q_f={q_gen_6821},
Delta=
{
<nil>() -> q_gen_6832
<b>() -> q_gen_6833
<nil, nil>() -> q_gen_6826
<a, a>() -> q_gen_6827
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, cons, nil>(q_gen_6833, q_gen_6832) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6823, q_gen_6824, q_gen_6828},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6823
<cons>(q_gen_6824, q_gen_6823) -> q_gen_6823
<a>() -> q_gen_6824
<a, cons>(q_gen_6824, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6823) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6819) -> q_gen_6828
<b, nil>() -> q_gen_6828
}

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

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 7
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 7
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]), {
_mla -> nil  ;  _nla -> nil  ;  h1 -> b  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.016400 s (model generation: 0.014187,  model checking: 0.002213):

Model:
|_
{
append -> 
{{{
Q={q_gen_6821, q_gen_6826, q_gen_6827, q_gen_6832, q_gen_6833},
Q_f={q_gen_6821},
Delta=
{
<nil>() -> q_gen_6832
<b>() -> q_gen_6833
<nil, nil>() -> q_gen_6826
<a, a>() -> q_gen_6827
<b, b>() -> q_gen_6827
<cons, nil, cons>(q_gen_6827, q_gen_6826) -> q_gen_6821
<nil, cons, nil>(q_gen_6833, q_gen_6832) -> q_gen_6821
<nil, nil, nil>() -> q_gen_6821
}

Datatype: <eltlist, eltlist, eltlist>
Convolution form: right
}}}
  ;  member -> 
{{{
Q={q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6823, q_gen_6824, q_gen_6828},
Q_f={q_gen_6818},
Delta=
{
<nil>() -> q_gen_6819
<b>() -> q_gen_6820
<cons>(q_gen_6820, q_gen_6819) -> q_gen_6823
<cons>(q_gen_6824, q_gen_6823) -> q_gen_6823
<a>() -> q_gen_6824
<a, cons>(q_gen_6824, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6820, q_gen_6819) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6823) -> q_gen_6818
<b, cons>(q_gen_6824, q_gen_6819) -> q_gen_6828
<b, nil>() -> q_gen_6828
}

Datatype: <elt, eltlist>
Convolution form: right
}}}
  ;  reverse -> 
{{{
Q={q_gen_6817, q_gen_6839, q_gen_6840},
Q_f={q_gen_6817},
Delta=
{
<nil>() -> q_gen_6839
<b>() -> q_gen_6840
<cons, nil>(q_gen_6840, q_gen_6839) -> q_gen_6817
<nil, nil>() -> q_gen_6817
}

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

}
--
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([_mla, cons(h1, nil), _nla]) /\ reverse([t1, _mla])) -> reverse([cons(h1, t1), _nla]) -> 7
(append([t1, l2, _hla])) -> append([cons(h1, t1), l2, cons(h1, _hla)]) -> 7
(member([e, l1]) /\ reverse([l1, _rla])) -> member([e, _rla]) -> 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, _rla])) -> member([e, _rla]), {
_rla -> nil  ;  e -> b  ;  l1 -> cons(b, nil)
})

Total time: 0.178735
Reason for stopping: Disproved