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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)])}
(append([_hh, _ih, _jh]) /\ append([_hh, _ih, _kh])) -> eq_natlist([_jh, _kh])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(append([cons(i, l1), l2, _lh])) -> not_null([_lh])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 0
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 60.000042 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1588, q_gen_1589, q_gen_1590, q_gen_1594, q_gen_1595, q_gen_1596, q_gen_1597, q_gen_1598, q_gen_1599, q_gen_1600, q_gen_1601, q_gen_1602, q_gen_1603, q_gen_1604, q_gen_1605, q_gen_1606, q_gen_1607, q_gen_1608, q_gen_1609, q_gen_1610, q_gen_1611, q_gen_1612, q_gen_1613, q_gen_1614, q_gen_1615, q_gen_1616, q_gen_1617, q_gen_1618, q_gen_1619, q_gen_1620, q_gen_1621, q_gen_1622, q_gen_1623, q_gen_1624, q_gen_1625, q_gen_1626, q_gen_1627, q_gen_1628, q_gen_1629, q_gen_1630, q_gen_1631, q_gen_1632, q_gen_1633, q_gen_1634, q_gen_1635, q_gen_1636, q_gen_1637, q_gen_1638, q_gen_1639, q_gen_1640, q_gen_1641, q_gen_1642, q_gen_1643, q_gen_1644, q_gen_1645, q_gen_1646, q_gen_1647, q_gen_1648, q_gen_1649, q_gen_1650, q_gen_1651, q_gen_1652, q_gen_1653, q_gen_1654, q_gen_1655, q_gen_1656, q_gen_1657},
Q_f={},
Delta=
{
<nil>() -> q_gen_1600
<z>() -> q_gen_1601
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1608
<s>(q_gen_1601) -> q_gen_1614
<s>(q_gen_1614) -> q_gen_1636
<nil, nil>() -> q_gen_1589
<z, z>() -> q_gen_1590
<cons, cons>(q_gen_1596, q_gen_1589) -> q_gen_1595
<s, s>(q_gen_1590) -> q_gen_1596
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1604
<cons, cons>(q_gen_1596, q_gen_1604) -> q_gen_1621
<nil, cons>(q_gen_1614, q_gen_1608) -> q_gen_1624
<s, z>(q_gen_1601) -> q_gen_1625
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1640
<z, s>(q_gen_1601) -> q_gen_1643
<nil, nil, nil>() -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1588
<nil, cons, cons>(q_gen_1596, q_gen_1595) -> q_gen_1594
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1597
<cons, cons, cons>(q_gen_1602, q_gen_1599) -> q_gen_1598
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1599
<z, z, z>() -> q_gen_1602
<cons, nil, cons>(q_gen_1590, q_gen_1604) -> q_gen_1603
<nil, cons, cons>(q_gen_1590, q_gen_1604) -> q_gen_1605
<cons, cons, cons>(q_gen_1602, q_gen_1607) -> q_gen_1606
<nil, nil, cons>(q_gen_1601, q_gen_1608) -> q_gen_1607
<cons, cons, cons>(q_gen_1610, q_gen_1607) -> q_gen_1609
<s, z, s>(q_gen_1590) -> q_gen_1610
<nil, cons, cons>(q_gen_1596, q_gen_1604) -> q_gen_1611
<cons, cons, cons>(q_gen_1615, q_gen_1613) -> q_gen_1612
<nil, nil, cons>(q_gen_1614, q_gen_1608) -> q_gen_1613
<s, s, s>(q_gen_1602) -> q_gen_1615
<cons, cons, cons>(q_gen_1615, q_gen_1599) -> q_gen_1616
<cons, cons, cons>(q_gen_1619, q_gen_1618) -> q_gen_1617
<cons, nil, cons>(q_gen_1596, q_gen_1604) -> q_gen_1618
<z, s, z>(q_gen_1601) -> q_gen_1619
<nil, cons, cons>(q_gen_1590, q_gen_1621) -> q_gen_1620
<cons, cons, cons>(q_gen_1610, q_gen_1623) -> q_gen_1622
<nil, cons, cons>(q_gen_1625, q_gen_1624) -> q_gen_1623
<cons, cons, cons>(q_gen_1628, q_gen_1627) -> q_gen_1626
<nil, cons, cons>(q_gen_1625, q_gen_1604) -> q_gen_1627
<s, z, s>(q_gen_1625) -> q_gen_1628
<cons, cons, cons>(q_gen_1602, q_gen_1630) -> q_gen_1629
<cons, cons, cons>(q_gen_1631, q_gen_1607) -> q_gen_1630
<s, s, s>(q_gen_1632) -> q_gen_1631
<s, z, z>(q_gen_1601) -> q_gen_1632
<cons, cons, cons>(q_gen_1628, q_gen_1634) -> q_gen_1633
<cons, cons, cons>(q_gen_1635, q_gen_1588) -> q_gen_1634
<z, s, z>(q_gen_1636) -> q_gen_1635
<cons, cons, cons>(q_gen_1610, q_gen_1638) -> q_gen_1637
<cons, cons, cons>(q_gen_1641, q_gen_1639) -> q_gen_1638
<cons, nil, cons>(q_gen_1590, q_gen_1640) -> q_gen_1639
<s, s, s>(q_gen_1642) -> q_gen_1641
<s, s, z>(q_gen_1643) -> q_gen_1642
<cons, cons, cons>(q_gen_1628, q_gen_1645) -> q_gen_1644
<cons, cons, cons>(q_gen_1647, q_gen_1646) -> q_gen_1645
<nil, cons, cons>(q_gen_1625, q_gen_1589) -> q_gen_1646
<s, z, s>(q_gen_1643) -> q_gen_1647
<cons, cons, cons>(q_gen_1602, q_gen_1649) -> q_gen_1648
<cons, cons, cons>(q_gen_1628, q_gen_1650) -> q_gen_1649
<cons, cons, cons>(q_gen_1651, q_gen_1599) -> q_gen_1650
<s, s, s>(q_gen_1652) -> q_gen_1651
<z, z, s>(q_gen_1601) -> q_gen_1652
<cons, cons, cons>(q_gen_1652, q_gen_1654) -> q_gen_1653
<nil, cons, cons>(q_gen_1625, q_gen_1640) -> q_gen_1654
<cons, cons, cons>(q_gen_1602, q_gen_1656) -> q_gen_1655
<cons, cons, cons>(q_gen_1657, q_gen_1605) -> q_gen_1656
<z, s, s>(q_gen_1590) -> q_gen_1657
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586, q_gen_1591, q_gen_1592, q_gen_1593},
Q_f={},
Delta=
{
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<z>() -> q_gen_1586
<cons>(q_gen_1586, q_gen_1592) -> q_gen_1591
<cons>(q_gen_1593, q_gen_1585) -> q_gen_1592
<s>(q_gen_1586) -> q_gen_1593
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.007245 s (model generation: 0.006275,  model checking: 0.000970):

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

}

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

}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 3
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 1
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> z
})

-------------------------------------------
Step 1, which took 0.005770 s (model generation: 0.005569,  model checking: 0.000201):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<nil>() -> q_gen_1584
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 1
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.004980 s (model generation: 0.004949,  model checking: 0.000031):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<nil>() -> q_gen_1584
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 1
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.005929 s (model generation: 0.005316,  model checking: 0.000613):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 4
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 2
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.006330 s (model generation: 0.005249,  model checking: 0.001081):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590},
Q_f={q_gen_1587},
Delta=
{
<nil, nil>() -> q_gen_1589
<z, z>() -> q_gen_1590
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 6
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 4
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 3
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> cons(s(z), nil)  ;  x -> z
})

-------------------------------------------
Step 5, which took 0.006858 s (model generation: 0.006176,  model checking: 0.000682):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590},
Q_f={q_gen_1587},
Delta=
{
<nil, nil>() -> q_gen_1589
<z, z>() -> q_gen_1590
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 4
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 6, which took 0.007075 s (model generation: 0.005286,  model checking: 0.001789):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590},
Q_f={q_gen_1587},
Delta=
{
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 7
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 5
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.009093 s (model generation: 0.007584,  model checking: 0.001509):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<nil>() -> q_gen_1600
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> not_null([cons(x, ll)]) -> 7
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 10
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 6
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.008147 s (model generation: 0.006145,  model checking: 0.002002):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<nil>() -> q_gen_1600
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> not_null([cons(x, ll)]) -> 8
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 13
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 7
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.010305 s (model generation: 0.006583,  model checking: 0.003722):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> not_null([cons(x, ll)]) -> 9
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 16
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 8
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.011334 s (model generation: 0.007790,  model checking: 0.003544):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, z, s>(q_gen_1590) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> not_null([cons(x, ll)]) -> 10
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 19
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 9
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.012435 s (model generation: 0.009124,  model checking: 0.003311):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<s>(q_gen_1601) -> q_gen_1601
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, s, s>(q_gen_1602) -> q_gen_1602
<s, z, s>(q_gen_1590) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> not_null([cons(x, ll)]) -> 11
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 22
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 10
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(s(z), cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 12, which took 0.018839 s (model generation: 0.012400,  model checking: 0.006439):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<s>(q_gen_1601) -> q_gen_1601
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, s, s>(q_gen_1602) -> q_gen_1602
<s, z, s>(q_gen_1590) -> q_gen_1602
<z, s, z>(q_gen_1601) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> not_null([cons(x, ll)]) -> 12
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 25
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 11
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, cons(s(z), cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.028927 s (model generation: 0.012401,  model checking: 0.016526):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<s>(q_gen_1601) -> q_gen_1601
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<s, z>(q_gen_1601) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, s, s>(q_gen_1602) -> q_gen_1602
<s, z, s>(q_gen_1590) -> q_gen_1602
<z, s, z>(q_gen_1601) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> not_null([cons(x, ll)]) -> 13
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 28
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 12
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(s(z), cons(z, cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 14, which took 0.033630 s (model generation: 0.017810,  model checking: 0.015820):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<s>(q_gen_1601) -> q_gen_1601
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<s, z>(q_gen_1601) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, s, s>(q_gen_1602) -> q_gen_1602
<s, z, s>(q_gen_1590) -> q_gen_1602
<s, z, z>(q_gen_1601) -> q_gen_1602
<z, s, z>(q_gen_1601) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> not_null([cons(x, ll)]) -> 14
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 31
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 13
(not_null([nil])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(s(z), cons(z, cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(s(s(z))), nil))  ;  t1 -> cons(s(s(z)), cons(z, cons(z, nil)))
})

-------------------------------------------
Step 15, which took 0.057776 s (model generation: 0.027080,  model checking: 0.030696):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<s>(q_gen_1601) -> q_gen_1601
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<s, z>(q_gen_1601) -> q_gen_1590
<z, s>(q_gen_1601) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, s, s>(q_gen_1602) -> q_gen_1602
<s, s, z>(q_gen_1590) -> q_gen_1602
<s, z, s>(q_gen_1590) -> q_gen_1602
<s, z, z>(q_gen_1601) -> q_gen_1602
<z, s, z>(q_gen_1601) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> not_null([cons(x, ll)]) -> 15
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 34
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 14
(not_null([nil])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(s(z), cons(s(s(z)), cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(z, cons(s(z), nil)))  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 16, which took 0.061921 s (model generation: 0.040346,  model checking: 0.021575):

Model:
|_
{
append -> 
{{{
Q={q_gen_1587, q_gen_1589, q_gen_1590, q_gen_1600, q_gen_1601, q_gen_1602},
Q_f={q_gen_1587},
Delta=
{
<cons>(q_gen_1601, q_gen_1600) -> q_gen_1600
<nil>() -> q_gen_1600
<s>(q_gen_1601) -> q_gen_1601
<z>() -> q_gen_1601
<cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1589
<nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1589
<nil, nil>() -> q_gen_1589
<s, s>(q_gen_1590) -> q_gen_1590
<s, z>(q_gen_1601) -> q_gen_1590
<z, s>(q_gen_1601) -> q_gen_1590
<z, z>() -> q_gen_1590
<cons, cons, cons>(q_gen_1602, q_gen_1587) -> q_gen_1587
<cons, nil, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, cons, cons>(q_gen_1590, q_gen_1589) -> q_gen_1587
<nil, nil, cons>(q_gen_1601, q_gen_1600) -> q_gen_1587
<nil, nil, nil>() -> q_gen_1587
<s, s, s>(q_gen_1602) -> q_gen_1602
<s, s, z>(q_gen_1590) -> q_gen_1602
<s, z, s>(q_gen_1590) -> q_gen_1602
<s, z, z>(q_gen_1601) -> q_gen_1602
<z, s, z>(q_gen_1601) -> q_gen_1602
<z, z, s>(q_gen_1601) -> q_gen_1602
<z, z, z>() -> q_gen_1602
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_1584, q_gen_1585, q_gen_1586},
Q_f={q_gen_1584},
Delta=
{
<cons>(q_gen_1586, q_gen_1584) -> q_gen_1584
<cons>(q_gen_1586, q_gen_1585) -> q_gen_1584
<nil>() -> q_gen_1585
<s>(q_gen_1586) -> q_gen_1586
<z>() -> q_gen_1586
}

Datatype: <natlist>
Convolution form: right
}}}

}
--
Equality automata are defined for: {eq_nat, eq_natlist}
_|

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> not_null([cons(x, ll)]) -> 16
(append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 37
(append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 15
(not_null([nil])) -> BOT -> 15
}
Sat witness: Found: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(s(z), cons(z, cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(s(z), cons(z, nil)))  ;  t1 -> cons(z, nil)
})

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