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, l2])
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)])}
(append([_jca, _kca, _lca]) /\ append([_jca, _kca, _mca])) -> eq_eltlist([_lca, _mca])
)
}

properties:
{(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 0
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 0
}


Solving took 60.000044 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5644, q_gen_5645, q_gen_5646, q_gen_5647, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5652, q_gen_5653, q_gen_5654, q_gen_5655, q_gen_5656, q_gen_5657, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5661, q_gen_5662, q_gen_5663, q_gen_5664, q_gen_5665, q_gen_5666, q_gen_5667, q_gen_5668, q_gen_5669, q_gen_5670, q_gen_5671, q_gen_5672, q_gen_5673, q_gen_5674, q_gen_5675, q_gen_5676, q_gen_5677, q_gen_5678, q_gen_5679, q_gen_5680, q_gen_5681, q_gen_5682, q_gen_5683, q_gen_5684, q_gen_5685, q_gen_5686, q_gen_5687, q_gen_5688, q_gen_5689, q_gen_5690, q_gen_5691, q_gen_5692, q_gen_5693, q_gen_5694, q_gen_5695, q_gen_5696, q_gen_5697, q_gen_5698, q_gen_5699, q_gen_5700, q_gen_5701, q_gen_5702, q_gen_5703, q_gen_5704, q_gen_5705, q_gen_5706, q_gen_5707, q_gen_5708, q_gen_5709, q_gen_5710, q_gen_5711, q_gen_5712, q_gen_5713, q_gen_5714, q_gen_5715, q_gen_5716, q_gen_5717, q_gen_5718, q_gen_5719, q_gen_5720, q_gen_5721, q_gen_5722, q_gen_5723, q_gen_5724, q_gen_5725, q_gen_5726, q_gen_5727, q_gen_5728, q_gen_5729, q_gen_5730, q_gen_5731, q_gen_5732, q_gen_5733, q_gen_5734, q_gen_5735, q_gen_5736, q_gen_5737, q_gen_5738, q_gen_5739, q_gen_5740, q_gen_5741, q_gen_5742, q_gen_5743, q_gen_5744, q_gen_5745, q_gen_5746, q_gen_5747, q_gen_5748, q_gen_5749, q_gen_5750, q_gen_5751, q_gen_5752, q_gen_5753, q_gen_5754},
Q_f={},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5672
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5691
<cons>(q_gen_5659, q_gen_5672) -> q_gen_5740
<cons>(q_gen_5650, q_gen_5672) -> q_gen_5754
<nil, nil>() -> q_gen_5641
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5645, q_gen_5641) -> q_gen_5644
<a, a>() -> q_gen_5645
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5678
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5684
<b, a>() -> q_gen_5687
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5693
<cons, cons>(q_gen_5645, q_gen_5644) -> q_gen_5697
<cons, cons>(q_gen_5645, q_gen_5666) -> q_gen_5700
<nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5711
<nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5719
<a, b>() -> q_gen_5750
<nil, nil, nil>() -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5645, q_gen_5644) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5646
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5647
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<b, b, b>() -> q_gen_5651
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5652
<cons, cons, cons>(q_gen_5655, q_gen_5648) -> q_gen_5654
<a, b, a>() -> q_gen_5655
<nil, cons, cons>(q_gen_5645, q_gen_5641) -> q_gen_5656
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5657
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5661
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5662
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5663
<cons, cons, cons>(q_gen_5660, q_gen_5665) -> q_gen_5664
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5665
<cons, cons, cons>(q_gen_5651, q_gen_5652) -> q_gen_5667
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5668
<nil, cons, cons>(q_gen_5645, q_gen_5666) -> q_gen_5669
<cons, cons, cons>(q_gen_5673, q_gen_5671) -> q_gen_5670
<nil, nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5671
<a, a, a>() -> q_gen_5673
<cons, cons, cons>(q_gen_5673, q_gen_5669) -> q_gen_5674
<cons, cons, cons>(q_gen_5660, q_gen_5670) -> q_gen_5675
<cons, cons, cons>(q_gen_5655, q_gen_5677) -> q_gen_5676
<cons, nil, cons>(q_gen_5642, q_gen_5678) -> q_gen_5677
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5679
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5680
<cons, nil, cons>(q_gen_5645, q_gen_5641) -> q_gen_5681
<cons, nil, cons>(q_gen_5642, q_gen_5644) -> q_gen_5682
<nil, cons, cons>(q_gen_5645, q_gen_5684) -> q_gen_5683
<cons, cons, cons>(q_gen_5673, q_gen_5686) -> q_gen_5685
<nil, cons, cons>(q_gen_5687, q_gen_5653) -> q_gen_5686
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5688
<cons, cons, cons>(q_gen_5655, q_gen_5690) -> q_gen_5689
<nil, nil, cons>(q_gen_5659, q_gen_5691) -> q_gen_5690
<cons, nil, cons>(q_gen_5642, q_gen_5693) -> q_gen_5692
<cons, cons, cons>(q_gen_5673, q_gen_5639) -> q_gen_5694
<cons, cons, cons>(q_gen_5655, q_gen_5639) -> q_gen_5695
<nil, cons, cons>(q_gen_5645, q_gen_5697) -> q_gen_5696
<cons, cons, cons>(q_gen_5673, q_gen_5699) -> q_gen_5698
<nil, cons, cons>(q_gen_5645, q_gen_5700) -> q_gen_5699
<cons, cons, cons>(q_gen_5673, q_gen_5640) -> q_gen_5701
<cons, cons, cons>(q_gen_5655, q_gen_5640) -> q_gen_5702
<nil, cons, cons>(q_gen_5642, q_gen_5684) -> q_gen_5703
<cons, cons, cons>(q_gen_5655, q_gen_5705) -> q_gen_5704
<nil, cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5705
<cons, cons, cons>(q_gen_5660, q_gen_5707) -> q_gen_5706
<nil, cons, cons>(q_gen_5645, q_gen_5693) -> q_gen_5707
<cons, cons, cons>(q_gen_5673, q_gen_5709) -> q_gen_5708
<cons, cons, cons>(q_gen_5660, q_gen_5710) -> q_gen_5709
<nil, cons, cons>(q_gen_5687, q_gen_5711) -> q_gen_5710
<cons, cons, cons>(q_gen_5655, q_gen_5656) -> q_gen_5712
<cons, cons, cons>(q_gen_5651, q_gen_5714) -> q_gen_5713
<cons, cons, cons>(q_gen_5673, q_gen_5658) -> q_gen_5714
<cons, cons, cons>(q_gen_5660, q_gen_5668) -> q_gen_5715
<cons, cons, cons>(q_gen_5660, q_gen_5717) -> q_gen_5716
<cons, cons, cons>(q_gen_5651, q_gen_5665) -> q_gen_5717
<cons, nil, cons>(q_gen_5642, q_gen_5719) -> q_gen_5718
<cons, cons, cons>(q_gen_5660, q_gen_5652) -> q_gen_5720
<cons, cons, cons>(q_gen_5651, q_gen_5722) -> q_gen_5721
<nil, cons, cons>(q_gen_5645, q_gen_5653) -> q_gen_5722
<cons, cons, cons>(q_gen_5651, q_gen_5724) -> q_gen_5723
<cons, cons, cons>(q_gen_5660, q_gen_5690) -> q_gen_5724
<cons, cons, cons>(q_gen_5660, q_gen_5726) -> q_gen_5725
<nil, cons, cons>(q_gen_5642, q_gen_5693) -> q_gen_5726
<cons, cons, cons>(q_gen_5660, q_gen_5728) -> q_gen_5727
<cons, cons, cons>(q_gen_5651, q_gen_5729) -> q_gen_5728
<nil, cons, cons>(q_gen_5642, q_gen_5711) -> q_gen_5729
<cons, cons, cons>(q_gen_5660, q_gen_5731) -> q_gen_5730
<cons, cons, cons>(q_gen_5655, q_gen_5732) -> q_gen_5731
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5732
<cons, cons, cons>(q_gen_5660, q_gen_5734) -> q_gen_5733
<cons, cons, cons>(q_gen_5651, q_gen_5735) -> q_gen_5734
<cons, cons, cons>(q_gen_5655, q_gen_5736) -> q_gen_5735
<nil, nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5736
<nil, cons, cons>(q_gen_5645, q_gen_5719) -> q_gen_5737
<cons, cons, cons>(q_gen_5673, q_gen_5739) -> q_gen_5738
<nil, nil, cons>(q_gen_5659, q_gen_5740) -> q_gen_5739
<cons, cons, cons>(q_gen_5651, q_gen_5742) -> q_gen_5741
<cons, cons, cons>(q_gen_5660, q_gen_5743) -> q_gen_5742
<cons, cons, cons>(q_gen_5673, q_gen_5732) -> q_gen_5743
<cons, cons, cons>(q_gen_5655, q_gen_5745) -> q_gen_5744
<cons, cons, cons>(q_gen_5660, q_gen_5746) -> q_gen_5745
<cons, cons, cons>(q_gen_5660, q_gen_5735) -> q_gen_5746
<nil, cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5747
<cons, cons, cons>(q_gen_5655, q_gen_5749) -> q_gen_5748
<nil, cons, cons>(q_gen_5750, q_gen_5666) -> q_gen_5749
<cons, cons, cons>(q_gen_5673, q_gen_5736) -> q_gen_5751
<cons, cons, cons>(q_gen_5651, q_gen_5753) -> q_gen_5752
<nil, nil, cons>(q_gen_5659, q_gen_5754) -> q_gen_5753
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.010309 s (model generation: 0.009838,  model checking: 0.000471):

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

}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 1
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 1, which took 0.011033 s (model generation: 0.010051,  model checking: 0.000982):

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 1
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.010982 s (model generation: 0.010403,  model checking: 0.000579):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642},
Q_f={q_gen_5639},
Delta=
{
<nil, nil>() -> q_gen_5641
<b, b>() -> q_gen_5642
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 2
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 3, which took 0.012774 s (model generation: 0.010781,  model checking: 0.001993):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642},
Q_f={q_gen_5639},
Delta=
{
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 3
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.014070 s (model generation: 0.012136,  model checking: 0.001934):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<b, b, b>() -> q_gen_5651
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 4
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 10
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.015513 s (model generation: 0.012643,  model checking: 0.002870):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<b, b, b>() -> q_gen_5651
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 5
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 6, which took 0.016817 s (model generation: 0.013512,  model checking: 0.003305):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 6
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 16
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.016309 s (model generation: 0.015911,  model checking: 0.000398):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<a>() -> q_gen_5650
<b>() -> q_gen_5650
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, a, b>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 9
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 16
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, nil)  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 8, which took 0.019923 s (model generation: 0.019411,  model checking: 0.000512):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<a>() -> q_gen_5650
<b>() -> q_gen_5650
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, a, b>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 12
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 16
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, cons(b, nil))  ;  i -> b  ;  j -> a  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 9, which took 0.021443 s (model generation: 0.020865,  model checking: 0.000578):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5644, q_gen_5646, q_gen_5649, q_gen_5650, q_gen_5651},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<a>() -> q_gen_5650
<b>() -> q_gen_5650
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5644
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5644
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5646
<cons, cons, cons>(q_gen_5651, q_gen_5646) -> q_gen_5646
<cons, nil, cons>(q_gen_5642, q_gen_5644) -> q_gen_5646
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5646
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5646
<a, b, a>() -> q_gen_5651
<b, a, b>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 12
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 16
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.029321 s (model generation: 0.019799,  model checking: 0.009522):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 13
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 19
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.028059 s (model generation: 0.024984,  model checking: 0.003075):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 14
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 22
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 12, which took 0.028240 s (model generation: 0.026185,  model checking: 0.002055):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5644, q_gen_5645, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<a>() -> q_gen_5650
<b>() -> q_gen_5650
<nil, nil>() -> q_gen_5641
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5645, q_gen_5641) -> q_gen_5644
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5644
<a, a>() -> q_gen_5645
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5645, q_gen_5644) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5644) -> q_gen_5648
<nil, cons, cons>(q_gen_5645, q_gen_5641) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 15
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 22
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.026980 s (model generation: 0.026090,  model checking: 0.000890):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5661},
Q_f={q_gen_5639, q_gen_5640},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5640
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5640
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5661
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 18
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 22
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, cons(a, nil))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.057332 s (model generation: 0.027891,  model checking: 0.029441):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 19
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 25
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.040508 s (model generation: 0.032529,  model checking: 0.007979):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 20
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 28
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.051720 s (model generation: 0.036397,  model checking: 0.015323):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 20
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 21
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 31
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 17, which took 0.360510 s (model generation: 0.036613,  model checking: 0.323897):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 21
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 22
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 34
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 18, which took 0.017843 s (model generation: 0.016957,  model checking: 0.000886):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639, q_gen_5640},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5640
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5640
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 25
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 34
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, cons(b, nil))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 19, which took 0.036490 s (model generation: 0.032983,  model checking: 0.003507):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5644, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5644
<cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5644
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5644
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5644) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 26
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 37
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 20, which took 0.433889 s (model generation: 0.064739,  model checking: 0.369150):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 27
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 40
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.034194 s (model generation: 0.032829,  model checking: 0.001365):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 30
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 40
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(a, nil)  ;  i -> a  ;  j -> b  ;  l1 -> nil
})

-------------------------------------------
Step 22, which took 1.030032 s (model generation: 0.079785,  model checking: 0.950247):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660, q_gen_5687},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5687, q_gen_5653) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 31
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 43
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.049951 s (model generation: 0.043330,  model checking: 0.006621):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5657, q_gen_5659, q_gen_5660, q_gen_5661, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5657},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5661) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5660, q_gen_5657) -> q_gen_5657
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5657
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5657
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5657) -> q_gen_5661
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5661
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5661
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5661
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 32
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 46
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.098385 s (model generation: 0.097724,  model checking: 0.000661):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5648
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, a, a>() -> q_gen_5651
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 35
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 46
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(a, nil)  ;  i -> b  ;  j -> a  ;  l1 -> cons(a, nil)
})

-------------------------------------------
Step 25, which took 0.089684 s (model generation: 0.088129,  model checking: 0.001555):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5644, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5662, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5644
<cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5644
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5644
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5662) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5644) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5643
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5662
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5644) -> q_gen_5662
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 36
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 49
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, cons(a, nil)))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.101546 s (model generation: 0.100389,  model checking: 0.001157):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5647, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5661, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5647},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5647
<cons, cons, cons>(q_gen_5660, q_gen_5647) -> q_gen_5647
<cons, cons, cons>(q_gen_5660, q_gen_5661) -> q_gen_5647
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5647
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5647
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5647) -> q_gen_5661
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5661
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5661
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5661
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 37
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 52
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 27, which took 0.095300 s (model generation: 0.094443,  model checking: 0.000857):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5662, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5640},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5660, q_gen_5662) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5640
<cons, cons, cons>(q_gen_5651, q_gen_5662) -> q_gen_5640
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5640
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5640
<a, a, a>() -> q_gen_5651
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5662
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5662
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5662
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 40
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 52
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(a, cons(b, nil))  ;  i -> b  ;  j -> a  ;  l1 -> cons(a, cons(b, nil))
})

-------------------------------------------
Step 28, which took 0.080859 s (model generation: 0.079078,  model checking: 0.001781):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5661, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5661) -> q_gen_5643
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5661
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5661
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5661
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5661
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 41
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 55
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 29, which took 0.119913 s (model generation: 0.117946,  model checking: 0.001967):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5662, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5640},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5662) -> q_gen_5640
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5640
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5662
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5662
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5662
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 42
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 58
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, cons(b, cons(a, nil))))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 30, which took 0.131606 s (model generation: 0.129726,  model checking: 0.001880):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5659, q_gen_5660, q_gen_5662, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5640},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5662) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5640
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5640
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5662
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5662
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 34
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 43
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 61
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 31, which took 0.200763 s (model generation: 0.198004,  model checking: 0.002759):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5640, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660, q_gen_5661, q_gen_5687},
Q_f={q_gen_5639, q_gen_5640},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5661) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5640
<cons, cons, cons>(q_gen_5660, q_gen_5640) -> q_gen_5640
<cons, cons, cons>(q_gen_5660, q_gen_5661) -> q_gen_5640
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5640
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5640
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5640) -> q_gen_5661
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5661
<nil, cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5661
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5661
<nil, cons, cons>(q_gen_5687, q_gen_5653) -> q_gen_5661
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 44
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 64
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 32, which took 0.185283 s (model generation: 0.181777,  model checking: 0.003506):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5648, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5687},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5648) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5648
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5648
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5648
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5648
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5648) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5653) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 45
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 67
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 33, which took 1.866547 s (model generation: 0.130056,  model checking: 1.736491):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5672, q_gen_5687},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5672
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5687, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 37
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 46
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 70
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 34, which took 0.171597 s (model generation: 0.169690,  model checking: 0.001907):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5652, q_gen_5653, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5687},
Q_f={q_gen_5639, q_gen_5652},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5653
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5652) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5652) -> q_gen_5652
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5652
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5652
<nil, cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5652
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5653) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 49
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 70
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, cons(b, cons(b, nil)))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 35, which took 0.171808 s (model generation: 0.169823,  model checking: 0.001985):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5644, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5644
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5644
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5643
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5643
<cons, nil, cons>(q_gen_5642, q_gen_5644) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5644) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 52
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 70
}
Sat witness: Found: ((append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]), {
_oca -> cons(b, cons(b, cons(a, nil)))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 36, which took 0.181631 s (model generation: 0.178820,  model checking: 0.002811):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5647, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5653, q_gen_5659, q_gen_5660, q_gen_5662, q_gen_5687},
Q_f={q_gen_5639, q_gen_5647},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5653
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5653
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5662) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5647) -> q_gen_5647
<cons, nil, cons>(q_gen_5642, q_gen_5653) -> q_gen_5647
<nil, cons, cons>(q_gen_5642, q_gen_5653) -> q_gen_5647
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5647
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5662
<cons, cons, cons>(q_gen_5660, q_gen_5647) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5662
<nil, cons, cons>(q_gen_5687, q_gen_5653) -> q_gen_5662
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 53
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 73
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 37, which took 0.327578 s (model generation: 0.322206,  model checking: 0.005372):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 54
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 76
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, cons(b, cons(a, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 38, which took 0.672220 s (model generation: 0.666452,  model checking: 0.005768):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 55
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 79
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, cons(b, cons(a, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, cons(b, nil)))  ;  t1 -> cons(b, cons(a, nil))
})

-------------------------------------------
Step 39, which took 2.983844 s (model generation: 0.655795,  model checking: 2.328049):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5672, q_gen_5687},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5672
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5687, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 43
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 56
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 82
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(a, cons(a, nil)))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 40, which took 0.630976 s (model generation: 0.619633,  model checking: 0.011343):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5643
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 44
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 57
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 85
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(b, cons(a, cons(b, cons(a, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, cons(a, cons(b, nil))))  ;  t1 -> cons(b, cons(b, cons(a, nil)))
})

-------------------------------------------
Step 41, which took 1.170150 s (model generation: 1.139871,  model checking: 0.030279):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<b, a>() -> q_gen_5687
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5643
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 45
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 58
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 88
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 42, which took 1.298998 s (model generation: 1.296860,  model checking: 0.002138):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5643, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5687},
Q_f={q_gen_5639, q_gen_5643},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<a, b>() -> q_gen_5687
<b, a>() -> q_gen_5687
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5643
<cons, cons, cons>(q_gen_5651, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5643) -> q_gen_5643
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5643
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5643
<nil, cons, cons>(q_gen_5687, q_gen_5666) -> q_gen_5643
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 46
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 59
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 91
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(b, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 43, which took 12.073262 s (model generation: 1.259473,  model checking: 10.813789):

Model:
|_
{
append -> 
{{{
Q={q_gen_5639, q_gen_5641, q_gen_5642, q_gen_5649, q_gen_5650, q_gen_5651, q_gen_5658, q_gen_5659, q_gen_5660, q_gen_5666, q_gen_5672, q_gen_5687},
Q_f={q_gen_5639},
Delta=
{
<cons>(q_gen_5650, q_gen_5649) -> q_gen_5649
<cons>(q_gen_5659, q_gen_5672) -> q_gen_5649
<nil>() -> q_gen_5649
<b>() -> q_gen_5650
<a>() -> q_gen_5659
<cons>(q_gen_5659, q_gen_5649) -> q_gen_5672
<cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5641
<nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5641
<nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5641
<nil, nil>() -> q_gen_5641
<a, a>() -> q_gen_5642
<b, b>() -> q_gen_5642
<cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5666
<nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5666
<nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5666
<a, b>() -> q_gen_5687
<b, a>() -> q_gen_5687
<cons, cons, cons>(q_gen_5651, q_gen_5639) -> q_gen_5639
<cons, cons, cons>(q_gen_5660, q_gen_5658) -> q_gen_5639
<cons, nil, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5642, q_gen_5641) -> q_gen_5639
<nil, cons, cons>(q_gen_5687, q_gen_5666) -> q_gen_5639
<nil, nil, cons>(q_gen_5650, q_gen_5649) -> q_gen_5639
<nil, nil, cons>(q_gen_5659, q_gen_5672) -> q_gen_5639
<nil, nil, nil>() -> q_gen_5639
<a, b, a>() -> q_gen_5651
<b, b, b>() -> q_gen_5651
<cons, cons, cons>(q_gen_5651, q_gen_5658) -> q_gen_5658
<cons, cons, cons>(q_gen_5660, q_gen_5639) -> q_gen_5658
<cons, nil, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5642, q_gen_5666) -> q_gen_5658
<nil, cons, cons>(q_gen_5687, q_gen_5641) -> q_gen_5658
<nil, nil, cons>(q_gen_5650, q_gen_5672) -> q_gen_5658
<nil, nil, cons>(q_gen_5659, q_gen_5649) -> q_gen_5658
<a, a, a>() -> q_gen_5660
<b, a, b>() -> q_gen_5660
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 47
(append([l1, cons(i, nil), _oca]) /\ append([l1, cons(j, nil), _oca])) -> eq_elt([i, j]) -> 60
(append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]) -> 94
}
Sat witness: Found: ((append([t1, l2, _ica])) -> append([cons(h1, t1), l2, cons(h1, _ica)]), {
_ica -> cons(a, cons(b, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

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