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


Learning problem is:

env: {
elt -> {a, b}  ;  eltlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)])}
(append([_qz, _rz, _sz]) /\ append([_qz, _rz, _tz])) -> eq_eltlist([_sz, _tz])
)
}

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


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

Clause system for inference is:

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


Solving took 60.000025 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6736, q_gen_6737, q_gen_6738, q_gen_6739, q_gen_6740, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6745, q_gen_6746, q_gen_6747, q_gen_6748, q_gen_6749, q_gen_6750, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6754, q_gen_6755, q_gen_6756, q_gen_6757, q_gen_6758, q_gen_6759, q_gen_6760, q_gen_6761, q_gen_6762, q_gen_6763, q_gen_6764, q_gen_6765, q_gen_6766, q_gen_6767, q_gen_6768, q_gen_6769, q_gen_6770, q_gen_6771, q_gen_6772, q_gen_6773, q_gen_6774, q_gen_6775, q_gen_6776, q_gen_6777, q_gen_6778, q_gen_6779, q_gen_6780, q_gen_6781, q_gen_6782, q_gen_6783, q_gen_6784, q_gen_6785, q_gen_6786, q_gen_6787, q_gen_6788, q_gen_6789, q_gen_6790, q_gen_6791, q_gen_6792, q_gen_6793, q_gen_6794, q_gen_6795, q_gen_6796, q_gen_6797, q_gen_6798, q_gen_6799, q_gen_6800, q_gen_6801, q_gen_6802, q_gen_6803, q_gen_6804, q_gen_6805, q_gen_6806, q_gen_6807, q_gen_6808, q_gen_6809, q_gen_6810, q_gen_6811, q_gen_6812, q_gen_6813, q_gen_6814, q_gen_6815, q_gen_6816, q_gen_6817, q_gen_6818, q_gen_6819, q_gen_6820, q_gen_6821, q_gen_6822, q_gen_6823, q_gen_6824, q_gen_6825, q_gen_6826, q_gen_6827},
Q_f={},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6765
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6784
<nil, nil>() -> q_gen_6734
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6738, q_gen_6734) -> q_gen_6737
<a, a>() -> q_gen_6738
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6771
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6777
<b, a>() -> q_gen_6780
<cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6786
<cons, cons>(q_gen_6738, q_gen_6737) -> q_gen_6790
<cons, cons>(q_gen_6738, q_gen_6759) -> q_gen_6793
<cons, cons>(q_gen_6738, q_gen_6800) -> q_gen_6799
<cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6800
<cons, cons>(q_gen_6780, q_gen_6805) -> q_gen_6804
<cons, cons>(q_gen_6806, q_gen_6759) -> q_gen_6805
<a, b>() -> q_gen_6806
<nil, cons>(q_gen_6743, q_gen_6765) -> q_gen_6825
<nil, nil, nil>() -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6738, q_gen_6737) -> q_gen_6736
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6739
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6740
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<b, b, b>() -> q_gen_6744
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6745
<cons, cons, cons>(q_gen_6748, q_gen_6741) -> q_gen_6747
<a, b, a>() -> q_gen_6748
<nil, cons, cons>(q_gen_6738, q_gen_6734) -> q_gen_6749
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6750
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6754
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6755
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6756
<cons, cons, cons>(q_gen_6753, q_gen_6758) -> q_gen_6757
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6758
<cons, cons, cons>(q_gen_6744, q_gen_6745) -> q_gen_6760
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6761
<nil, cons, cons>(q_gen_6738, q_gen_6759) -> q_gen_6762
<cons, cons, cons>(q_gen_6766, q_gen_6764) -> q_gen_6763
<nil, nil, cons>(q_gen_6752, q_gen_6765) -> q_gen_6764
<a, a, a>() -> q_gen_6766
<cons, cons, cons>(q_gen_6766, q_gen_6762) -> q_gen_6767
<cons, cons, cons>(q_gen_6753, q_gen_6763) -> q_gen_6768
<cons, cons, cons>(q_gen_6748, q_gen_6770) -> q_gen_6769
<cons, nil, cons>(q_gen_6735, q_gen_6771) -> q_gen_6770
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6772
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6773
<cons, nil, cons>(q_gen_6738, q_gen_6734) -> q_gen_6774
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6775
<nil, cons, cons>(q_gen_6738, q_gen_6777) -> q_gen_6776
<cons, cons, cons>(q_gen_6766, q_gen_6779) -> q_gen_6778
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6779
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6781
<cons, cons, cons>(q_gen_6748, q_gen_6783) -> q_gen_6782
<nil, nil, cons>(q_gen_6752, q_gen_6784) -> q_gen_6783
<cons, nil, cons>(q_gen_6735, q_gen_6786) -> q_gen_6785
<cons, cons, cons>(q_gen_6766, q_gen_6732) -> q_gen_6787
<cons, cons, cons>(q_gen_6748, q_gen_6732) -> q_gen_6788
<nil, cons, cons>(q_gen_6738, q_gen_6790) -> q_gen_6789
<cons, cons, cons>(q_gen_6753, q_gen_6792) -> q_gen_6791
<nil, cons, cons>(q_gen_6738, q_gen_6793) -> q_gen_6792
<cons, cons, cons>(q_gen_6748, q_gen_6781) -> q_gen_6794
<cons, cons, cons>(q_gen_6748, q_gen_6796) -> q_gen_6795
<cons, cons, cons>(q_gen_6748, q_gen_6751) -> q_gen_6796
<cons, cons, cons>(q_gen_6744, q_gen_6798) -> q_gen_6797
<nil, cons, cons>(q_gen_6780, q_gen_6799) -> q_gen_6798
<cons, cons, cons>(q_gen_6748, q_gen_6802) -> q_gen_6801
<cons, cons, cons>(q_gen_6744, q_gen_6803) -> q_gen_6802
<nil, cons, cons>(q_gen_6738, q_gen_6804) -> q_gen_6803
<cons, cons, cons>(q_gen_6753, q_gen_6808) -> q_gen_6807
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6808
<cons, cons, cons>(q_gen_6753, q_gen_6810) -> q_gen_6809
<cons, cons, cons>(q_gen_6744, q_gen_6811) -> q_gen_6810
<nil, nil, cons>(q_gen_6743, q_gen_6765) -> q_gen_6811
<cons, cons, cons>(q_gen_6753, q_gen_6745) -> q_gen_6812
<cons, cons, cons>(q_gen_6744, q_gen_6758) -> q_gen_6813
<nil, cons, cons>(q_gen_6806, q_gen_6734) -> q_gen_6814
<cons, cons, cons>(q_gen_6753, q_gen_6816) -> q_gen_6815
<cons, nil, cons>(q_gen_6735, q_gen_6777) -> q_gen_6816
<nil, cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6817
<cons, cons, cons>(q_gen_6748, q_gen_6819) -> q_gen_6818
<nil, nil, cons>(q_gen_6743, q_gen_6784) -> q_gen_6819
<cons, cons, cons>(q_gen_6753, q_gen_6821) -> q_gen_6820
<nil, cons, cons>(q_gen_6738, q_gen_6786) -> q_gen_6821
<cons, cons, cons>(q_gen_6753, q_gen_6823) -> q_gen_6822
<cons, cons, cons>(q_gen_6753, q_gen_6824) -> q_gen_6823
<nil, cons, cons>(q_gen_6780, q_gen_6825) -> q_gen_6824
<cons, cons, cons>(q_gen_6748, q_gen_6817) -> q_gen_6826
<cons, cons, cons>(q_gen_6744, q_gen_6818) -> q_gen_6827
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008607 s (model generation: 0.008335,  model checking: 0.000272):

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

}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 1
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 1, which took 0.007464 s (model generation: 0.007304,  model checking: 0.000160):

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

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 1
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 4
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> nil  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 2, which took 0.015679 s (model generation: 0.013729,  model checking: 0.001950):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735},
Q_f={q_gen_6732},
Delta=
{
<nil, nil>() -> q_gen_6734
<b, b>() -> q_gen_6735
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 2
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, cons(a, nil))
})

-------------------------------------------
Step 3, which took 0.010241 s (model generation: 0.008963,  model checking: 0.001278):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735},
Q_f={q_gen_6732},
Delta=
{
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 3
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 7
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.011276 s (model generation: 0.009834,  model checking: 0.001442):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<b, b, b>() -> q_gen_6744
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 4
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 10
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 5, which took 0.010766 s (model generation: 0.008797,  model checking: 0.001969):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<b, b, b>() -> q_gen_6744
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 5
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 13
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, nil)  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 6, which took 0.012127 s (model generation: 0.010013,  model checking: 0.002114):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 6
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 16
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, nil)  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.013010 s (model generation: 0.012431,  model checking: 0.000579):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<a>() -> q_gen_6743
<b>() -> q_gen_6743
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, a, b>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 9
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 16
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, nil)  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 8, which took 0.013286 s (model generation: 0.013108,  model checking: 0.000178):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<a>() -> q_gen_6743
<b>() -> q_gen_6743
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, a, b>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 12
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 16
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, cons(b, nil))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 9, which took 0.015312 s (model generation: 0.014196,  model checking: 0.001116):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6737, q_gen_6739, q_gen_6742, q_gen_6743, q_gen_6744},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<a>() -> q_gen_6743
<b>() -> q_gen_6743
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6737
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6737
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6739
<cons, cons, cons>(q_gen_6744, q_gen_6739) -> q_gen_6739
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6739
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6739
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6739
<a, b, a>() -> q_gen_6744
<b, a, b>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 12
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 16
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(b, nil)
})

-------------------------------------------
Step 10, which took 0.025263 s (model generation: 0.018956,  model checking: 0.006307):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 13
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 19
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 11, which took 0.018790 s (model generation: 0.016961,  model checking: 0.001829):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 14
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 22
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 12, which took 0.026314 s (model generation: 0.025221,  model checking: 0.001093):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6737, q_gen_6738, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<a>() -> q_gen_6743
<b>() -> q_gen_6743
<nil, nil>() -> q_gen_6734
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6738, q_gen_6734) -> q_gen_6737
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6737
<a, a>() -> q_gen_6738
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6738, q_gen_6737) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6741
<nil, cons, cons>(q_gen_6738, q_gen_6734) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 15
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 22
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(a, nil)
})

-------------------------------------------
Step 13, which took 0.022998 s (model generation: 0.022552,  model checking: 0.000446):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753, q_gen_6754},
Q_f={q_gen_6732, q_gen_6733},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6733
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6733
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6754
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 18
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 22
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, cons(a, nil))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, nil)
})

-------------------------------------------
Step 14, which took 0.034535 s (model generation: 0.019871,  model checking: 0.014664):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 19
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 25
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.029134 s (model generation: 0.025020,  model checking: 0.004114):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6759},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 20
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 28
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 16, which took 0.033031 s (model generation: 0.025528,  model checking: 0.007503):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6759},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6751
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 21
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 31
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(a, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 17, which took 0.436747 s (model generation: 0.027528,  model checking: 0.409219):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 22
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 34
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(b, cons(b, nil)))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 18, which took 0.035190 s (model generation: 0.034006,  model checking: 0.001184):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732, q_gen_6733},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6733
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6733
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 25
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 34
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, cons(b, nil))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 19, which took 0.043021 s (model generation: 0.040988,  model checking: 0.002033):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6737, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6737
<cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6737
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6737
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 26
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 37
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 20, which took 0.510757 s (model generation: 0.043495,  model checking: 0.467262):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 27
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 40
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.054215 s (model generation: 0.053002,  model checking: 0.001213):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 30
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 40
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(a, nil)  ;  i -> a  ;  j -> b  ;  l1 -> nil
})

-------------------------------------------
Step 22, which took 1.235695 s (model generation: 0.056065,  model checking: 1.179630):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753, q_gen_6780},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 31
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 43
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 23, which took 0.070962 s (model generation: 0.066860,  model checking: 0.004102):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6750, q_gen_6752, q_gen_6753, q_gen_6754, q_gen_6759, q_gen_6780},
Q_f={q_gen_6732, q_gen_6750},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6754) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6753, q_gen_6750) -> q_gen_6750
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6750
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6750
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6750) -> q_gen_6754
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6754
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6754
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6754
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 32
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 46
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(a, nil))  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 24, which took 0.076514 s (model generation: 0.075295,  model checking: 0.001219):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6759, q_gen_6780},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6741
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, a, a>() -> q_gen_6744
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6751
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 35
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 46
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(a, nil)  ;  i -> b  ;  j -> a  ;  l1 -> cons(a, nil)
})

-------------------------------------------
Step 25, which took 0.081945 s (model generation: 0.079361,  model checking: 0.002584):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6736, q_gen_6737, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753, q_gen_6755, q_gen_6780},
Q_f={q_gen_6732, q_gen_6736},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6737
<cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6737
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6737
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6736) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6755) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6736
<nil, cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6736
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6736
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6755
<cons, cons, cons>(q_gen_6753, q_gen_6736) -> q_gen_6755
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6755
<nil, cons, cons>(q_gen_6780, q_gen_6737) -> q_gen_6755
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 36
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 49
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(a, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, cons(a, nil)))  ;  t1 -> nil
})

-------------------------------------------
Step 26, which took 0.128951 s (model generation: 0.099979,  model checking: 0.028972):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753, q_gen_6755, q_gen_6780},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6755) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6755
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6755
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6755
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 37
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 52
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(a, nil))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

-------------------------------------------
Step 27, which took 0.200680 s (model generation: 0.117698,  model checking: 0.082982):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6737, q_gen_6740, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753, q_gen_6755, q_gen_6780},
Q_f={q_gen_6732, q_gen_6740},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6737
<cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6737
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6737
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6755) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6740) -> q_gen_6740
<cons, cons, cons>(q_gen_6744, q_gen_6755) -> q_gen_6740
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6740
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6740
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6755
<cons, cons, cons>(q_gen_6753, q_gen_6740) -> q_gen_6755
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6755
<nil, cons, cons>(q_gen_6780, q_gen_6737) -> q_gen_6755
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 38
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 55
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(a, cons(a, cons(b, cons(a, nil)))))  ;  h1 -> a  ;  l2 -> cons(b, cons(b, cons(a, cons(b, cons(a, nil)))))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 28, which took 0.176446 s (model generation: 0.172623,  model checking: 0.003823):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6750, q_gen_6752, q_gen_6753, q_gen_6754, q_gen_6759, q_gen_6780},
Q_f={q_gen_6732, q_gen_6750},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6759) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6759
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6754) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6754) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6753, q_gen_6750) -> q_gen_6750
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6750
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6750
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6750
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6750) -> q_gen_6754
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6754
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6754
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 39
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 58
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(b, cons(a, nil)))  ;  h1 -> b  ;  l2 -> cons(a, cons(b, nil))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 29, which took 0.320160 s (model generation: 0.318606,  model checking: 0.001554):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6736, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6780},
Q_f={q_gen_6732, q_gen_6736},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6746
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6736) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6736) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6736
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6736
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6736
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6736
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<nil, cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 42
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 58
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, cons(b, cons(b, nil)))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 30, which took 0.299430 s (model generation: 0.297597,  model checking: 0.001833):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6736, q_gen_6737, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6780},
Q_f={q_gen_6732, q_gen_6736},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6737) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6737
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6737
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6737
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6753, q_gen_6736) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6736
<cons, cons, cons>(q_gen_6744, q_gen_6736) -> q_gen_6736
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6736
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6736
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6736
<nil, cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6736
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6737) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 45
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 58
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, cons(b, cons(a, nil)))  ;  i -> a  ;  j -> b  ;  l1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 31, which took 0.286977 s (model generation: 0.285666,  model checking: 0.001311):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6752, q_gen_6753, q_gen_6754, q_gen_6780},
Q_f={q_gen_6732, q_gen_6733},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<a, b>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6753, q_gen_6754) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6733
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6733
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6733
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6733
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6754
<cons, cons, cons>(q_gen_6744, q_gen_6754) -> q_gen_6754
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6754
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6754
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6754
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 48
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 58
}
Sat witness: Found: ((append([l1, cons(i, nil), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]), {
_vz -> cons(b, nil)  ;  i -> b  ;  j -> a  ;  l1 -> nil
})

-------------------------------------------
Step 32, which took 0.350420 s (model generation: 0.347797,  model checking: 0.002623):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6737, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6780},
Q_f={q_gen_6732, q_gen_6733},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6737
<cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6737
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6737
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, nil, cons>(q_gen_6735, q_gen_6737) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6733
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6733
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6733
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6737) -> q_gen_6733
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6751
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6737) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 49
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 61
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(b, nil))  ;  h1 -> b  ;  l2 -> cons(a, nil)  ;  t1 -> cons(b, cons(b, nil))
})

-------------------------------------------
Step 33, which took 0.456172 s (model generation: 0.453162,  model checking: 0.003010):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6780},
Q_f={q_gen_6732, q_gen_6733},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6733
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6733
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6751
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 50
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 64
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, nil)  ;  h1 -> b  ;  l2 -> cons(b, nil)  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 34, which took 0.377648 s (model generation: 0.374876,  model checking: 0.002772):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6759, q_gen_6765, q_gen_6780},
Q_f={q_gen_6732},
Delta=
{
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6765
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6765
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6759) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6759
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6759
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6765) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6751
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6751
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6751
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6751
<nil, nil, cons>(q_gen_6743, q_gen_6765) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 51
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 67
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(b, nil))  ;  h1 -> a  ;  l2 -> cons(b, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.512405 s (model generation: 0.504961,  model checking: 0.007444):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6733, q_gen_6734, q_gen_6735, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753, q_gen_6755, q_gen_6759, q_gen_6780},
Q_f={q_gen_6732, q_gen_6733},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6759) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6759
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6759
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6733) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6755) -> q_gen_6733
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6733
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6733
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6755
<cons, cons, cons>(q_gen_6744, q_gen_6755) -> q_gen_6755
<cons, cons, cons>(q_gen_6753, q_gen_6733) -> q_gen_6755
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6755
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6755
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6755
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 52
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 70
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(b, cons(a, cons(b, cons(a, nil))))  ;  h1 -> b  ;  l2 -> cons(a, cons(a, cons(b, nil)))  ;  t1 -> cons(b, nil)
})

-------------------------------------------
Step 36, which took 0.713947 s (model generation: 0.711775,  model checking: 0.002172):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6740, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6752, q_gen_6753, q_gen_6754, q_gen_6759, q_gen_6780},
Q_f={q_gen_6732, q_gen_6740},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<cons, cons>(q_gen_6780, q_gen_6759) -> q_gen_6734
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6759
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6759
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6759
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6740
<cons, cons, cons>(q_gen_6753, q_gen_6740) -> q_gen_6740
<cons, cons, cons>(q_gen_6753, q_gen_6754) -> q_gen_6740
<nil, cons, cons>(q_gen_6735, q_gen_6759) -> q_gen_6740
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6740
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
<cons, cons, cons>(q_gen_6744, q_gen_6740) -> q_gen_6754
<cons, cons, cons>(q_gen_6744, q_gen_6754) -> q_gen_6754
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6754
<cons, nil, cons>(q_gen_6735, q_gen_6759) -> q_gen_6754
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6754
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 53
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 73
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, nil)  ;  h1 -> b  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 37, which took 0.763633 s (model generation: 0.759589,  model checking: 0.004044):

Model:
|_
{
append -> 
{{{
Q={q_gen_6732, q_gen_6734, q_gen_6735, q_gen_6741, q_gen_6742, q_gen_6743, q_gen_6744, q_gen_6746, q_gen_6751, q_gen_6752, q_gen_6753, q_gen_6780},
Q_f={q_gen_6732},
Delta=
{
<cons>(q_gen_6743, q_gen_6742) -> q_gen_6742
<cons>(q_gen_6752, q_gen_6742) -> q_gen_6742
<nil>() -> q_gen_6742
<b>() -> q_gen_6743
<a>() -> q_gen_6752
<cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6734
<nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6734
<nil, nil>() -> q_gen_6734
<a, a>() -> q_gen_6735
<b, b>() -> q_gen_6735
<cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6746
<cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6746
<cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6746
<nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6746
<a, b>() -> q_gen_6780
<b, a>() -> q_gen_6780
<cons, cons, cons>(q_gen_6744, q_gen_6741) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6732) -> q_gen_6732
<cons, cons, cons>(q_gen_6753, q_gen_6751) -> q_gen_6732
<cons, nil, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, cons, cons>(q_gen_6735, q_gen_6734) -> q_gen_6732
<nil, nil, nil>() -> q_gen_6732
<cons, cons, cons>(q_gen_6744, q_gen_6751) -> q_gen_6741
<cons, cons, cons>(q_gen_6753, q_gen_6741) -> q_gen_6741
<cons, nil, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, cons, cons>(q_gen_6735, q_gen_6746) -> q_gen_6741
<nil, nil, cons>(q_gen_6743, q_gen_6742) -> q_gen_6741
<a, b, a>() -> q_gen_6744
<b, b, b>() -> q_gen_6744
<cons, cons, cons>(q_gen_6744, q_gen_6732) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6734) -> q_gen_6751
<nil, cons, cons>(q_gen_6780, q_gen_6746) -> q_gen_6751
<nil, nil, cons>(q_gen_6752, q_gen_6742) -> q_gen_6751
<a, a, a>() -> q_gen_6753
<b, a, b>() -> q_gen_6753
}

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

}
--
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), _vz]) /\ append([l1, cons(j, nil), _vz])) -> eq_elt([i, j]) -> 54
(append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]) -> 76
}
Sat witness: Found: ((append([t1, l2, _pz])) -> append([cons(h1, t1), l2, cons(h1, _pz)]), {
_pz -> cons(a, cons(b, cons(b, nil)))  ;  h1 -> b  ;  l2 -> cons(b, cons(b, nil))  ;  t1 -> cons(a, nil)
})

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