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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)])}
(append([_yy, _zy, _az]) /\ append([_yy, _zy, _bz])) -> eq_natlist([_az, _bz])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

properties:
{(append([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz])}


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

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> not_null([cons(x, ll)]) -> 0
(append([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 0
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 0
(not_null([nil])) -> BOT -> 0
}


Solving took 60.000033 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6608, q_gen_6609, q_gen_6610, q_gen_6614, q_gen_6615, q_gen_6616, q_gen_6617, q_gen_6618, q_gen_6619, q_gen_6620, q_gen_6621, q_gen_6622, q_gen_6623, q_gen_6624, q_gen_6625, q_gen_6626, q_gen_6627, q_gen_6628, q_gen_6629, q_gen_6630, q_gen_6631, q_gen_6632, q_gen_6633, q_gen_6634, q_gen_6635, q_gen_6636, q_gen_6637, q_gen_6638, q_gen_6639, q_gen_6640, q_gen_6641, q_gen_6642, q_gen_6643, q_gen_6644, q_gen_6645, q_gen_6646, q_gen_6647, q_gen_6648, q_gen_6649, q_gen_6650, q_gen_6651, q_gen_6652, q_gen_6653, q_gen_6654, q_gen_6655, q_gen_6656, q_gen_6657, q_gen_6658, q_gen_6659, q_gen_6660, q_gen_6661, q_gen_6662, q_gen_6663, q_gen_6664, q_gen_6665, q_gen_6666, q_gen_6667, q_gen_6668, q_gen_6669, q_gen_6670, q_gen_6671, q_gen_6672, q_gen_6673, q_gen_6674, q_gen_6675, q_gen_6676, q_gen_6677, q_gen_6678, q_gen_6679, q_gen_6680},
Q_f={},
Delta=
{
<nil>() -> q_gen_6620
<z>() -> q_gen_6621
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6628
<s>(q_gen_6621) -> q_gen_6634
<s>(q_gen_6634) -> q_gen_6657
<nil, nil>() -> q_gen_6609
<z, z>() -> q_gen_6610
<cons, cons>(q_gen_6616, q_gen_6609) -> q_gen_6615
<s, s>(q_gen_6610) -> q_gen_6616
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6624
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6639
<cons, cons>(q_gen_6616, q_gen_6624) -> q_gen_6642
<nil, cons>(q_gen_6634, q_gen_6628) -> q_gen_6645
<s, z>(q_gen_6621) -> q_gen_6646
<z, s>(q_gen_6621) -> q_gen_6663
<s, z>(q_gen_6634) -> q_gen_6676
<nil, nil, nil>() -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6608
<nil, cons, cons>(q_gen_6616, q_gen_6615) -> q_gen_6614
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6617
<cons, cons, cons>(q_gen_6622, q_gen_6619) -> q_gen_6618
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6619
<z, z, z>() -> q_gen_6622
<cons, nil, cons>(q_gen_6610, q_gen_6624) -> q_gen_6623
<nil, cons, cons>(q_gen_6610, q_gen_6624) -> q_gen_6625
<cons, cons, cons>(q_gen_6622, q_gen_6627) -> q_gen_6626
<nil, nil, cons>(q_gen_6621, q_gen_6628) -> q_gen_6627
<cons, cons, cons>(q_gen_6630, q_gen_6627) -> q_gen_6629
<s, z, s>(q_gen_6610) -> q_gen_6630
<nil, cons, cons>(q_gen_6616, q_gen_6624) -> q_gen_6631
<cons, cons, cons>(q_gen_6635, q_gen_6633) -> q_gen_6632
<nil, nil, cons>(q_gen_6634, q_gen_6628) -> q_gen_6633
<s, s, s>(q_gen_6622) -> q_gen_6635
<cons, cons, cons>(q_gen_6635, q_gen_6608) -> q_gen_6636
<cons, cons, cons>(q_gen_6640, q_gen_6638) -> q_gen_6637
<cons, nil, cons>(q_gen_6616, q_gen_6639) -> q_gen_6638
<z, s, z>(q_gen_6621) -> q_gen_6640
<nil, cons, cons>(q_gen_6610, q_gen_6642) -> q_gen_6641
<cons, cons, cons>(q_gen_6622, q_gen_6644) -> q_gen_6643
<nil, cons, cons>(q_gen_6646, q_gen_6645) -> q_gen_6644
<cons, cons, cons>(q_gen_6649, q_gen_6648) -> q_gen_6647
<nil, cons, cons>(q_gen_6646, q_gen_6624) -> q_gen_6648
<s, z, s>(q_gen_6646) -> q_gen_6649
<cons, cons, cons>(q_gen_6622, q_gen_6651) -> q_gen_6650
<cons, cons, cons>(q_gen_6652, q_gen_6627) -> q_gen_6651
<s, s, s>(q_gen_6653) -> q_gen_6652
<s, z, z>(q_gen_6621) -> q_gen_6653
<cons, cons, cons>(q_gen_6649, q_gen_6655) -> q_gen_6654
<cons, cons, cons>(q_gen_6656, q_gen_6608) -> q_gen_6655
<z, s, z>(q_gen_6657) -> q_gen_6656
<cons, cons, cons>(q_gen_6630, q_gen_6659) -> q_gen_6658
<cons, cons, cons>(q_gen_6661, q_gen_6660) -> q_gen_6659
<cons, nil, cons>(q_gen_6610, q_gen_6639) -> q_gen_6660
<s, s, s>(q_gen_6662) -> q_gen_6661
<s, s, z>(q_gen_6663) -> q_gen_6662
<cons, cons, cons>(q_gen_6668, q_gen_6665) -> q_gen_6664
<cons, cons, cons>(q_gen_6667, q_gen_6666) -> q_gen_6665
<nil, cons, cons>(q_gen_6646, q_gen_6609) -> q_gen_6666
<s, z, s>(q_gen_6663) -> q_gen_6667
<s, z, s>(q_gen_6616) -> q_gen_6668
<cons, cons, cons>(q_gen_6622, q_gen_6670) -> q_gen_6669
<cons, cons, cons>(q_gen_6668, q_gen_6671) -> q_gen_6670
<cons, cons, cons>(q_gen_6672, q_gen_6619) -> q_gen_6671
<s, s, s>(q_gen_6673) -> q_gen_6672
<z, z, s>(q_gen_6621) -> q_gen_6673
<cons, cons, cons>(q_gen_6667, q_gen_6675) -> q_gen_6674
<nil, cons, cons>(q_gen_6676, q_gen_6624) -> q_gen_6675
<cons, cons, cons>(q_gen_6622, q_gen_6678) -> q_gen_6677
<cons, cons, cons>(q_gen_6679, q_gen_6627) -> q_gen_6678
<s, s, s>(q_gen_6680) -> q_gen_6679
<z, s, s>(q_gen_6610) -> q_gen_6680
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606, q_gen_6611, q_gen_6612, q_gen_6613},
Q_f={},
Delta=
{
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<z>() -> q_gen_6606
<cons>(q_gen_6606, q_gen_6612) -> q_gen_6611
<cons>(q_gen_6613, q_gen_6605) -> q_gen_6612
<s>(q_gen_6606) -> q_gen_6613
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.008478 s (model generation: 0.008292,  model checking: 0.000186):

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

}

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

}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 1
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> z
})

-------------------------------------------
Step 1, which took 0.008415 s (model generation: 0.008269,  model checking: 0.000146):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<nil>() -> q_gen_6604
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 1
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 1
(not_null([nil])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.009939 s (model generation: 0.009923,  model checking: 0.000016):

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

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<nil>() -> q_gen_6604
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 1
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 1
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.008712 s (model generation: 0.008536,  model checking: 0.000176):

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

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 1
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.010014 s (model generation: 0.009646,  model checking: 0.000368):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610},
Q_f={q_gen_6607},
Delta=
{
<nil, nil>() -> q_gen_6609
<z, z>() -> q_gen_6610
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 2
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 4
(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.010649 s (model generation: 0.010049,  model checking: 0.000600):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610},
Q_f={q_gen_6607},
Delta=
{
<nil, nil>() -> q_gen_6609
<z, z>() -> q_gen_6610
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 3
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 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.011575 s (model generation: 0.010036,  model checking: 0.001539):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610},
Q_f={q_gen_6607},
Delta=
{
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 4
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 7
(not_null([nil])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.012483 s (model generation: 0.011398,  model checking: 0.001085):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<nil>() -> q_gen_6620
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 5
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 10
(not_null([nil])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 8, which took 0.014220 s (model generation: 0.012315,  model checking: 0.001905):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<nil>() -> q_gen_6620
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 6
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 13
(not_null([nil])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 9, which took 0.016085 s (model generation: 0.012798,  model checking: 0.003287):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 7
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 16
(not_null([nil])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 10, which took 0.017348 s (model generation: 0.012980,  model checking: 0.004368):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, z, s>(q_gen_6610) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 8
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 19
(not_null([nil])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.021972 s (model generation: 0.016898,  model checking: 0.005074):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<s>(q_gen_6621) -> q_gen_6621
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, s, s>(q_gen_6622) -> q_gen_6622
<s, z, s>(q_gen_6610) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 9
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 22
(not_null([nil])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(s(z), cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 12, which took 0.027984 s (model generation: 0.019122,  model checking: 0.008862):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<s>(q_gen_6621) -> q_gen_6621
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, s, s>(q_gen_6622) -> q_gen_6622
<s, z, s>(q_gen_6610) -> q_gen_6622
<z, s, z>(q_gen_6621) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 10
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 25
(not_null([nil])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(z, cons(s(z), cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.046245 s (model generation: 0.022702,  model checking: 0.023543):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<s>(q_gen_6621) -> q_gen_6621
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<s, z>(q_gen_6621) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, s, s>(q_gen_6622) -> q_gen_6622
<s, z, s>(q_gen_6610) -> q_gen_6622
<z, s, z>(q_gen_6621) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 11
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 28
(not_null([nil])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> 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.048777 s (model generation: 0.029798,  model checking: 0.018979):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<s>(q_gen_6621) -> q_gen_6621
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<s, z>(q_gen_6621) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, s, s>(q_gen_6622) -> q_gen_6622
<s, z, s>(q_gen_6610) -> q_gen_6622
<s, z, z>(q_gen_6621) -> q_gen_6622
<z, s, z>(q_gen_6621) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 12
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 31
(not_null([nil])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> 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.084511 s (model generation: 0.045653,  model checking: 0.038858):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<s>(q_gen_6621) -> q_gen_6621
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<s, z>(q_gen_6621) -> q_gen_6610
<z, s>(q_gen_6621) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, s, s>(q_gen_6622) -> q_gen_6622
<s, s, z>(q_gen_6610) -> q_gen_6622
<s, z, s>(q_gen_6610) -> q_gen_6622
<s, z, z>(q_gen_6621) -> q_gen_6622
<z, s, z>(q_gen_6621) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 13
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 34
(not_null([nil])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(s(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.097951 s (model generation: 0.079151,  model checking: 0.018800):

Model:
|_
{
append -> 
{{{
Q={q_gen_6607, q_gen_6609, q_gen_6610, q_gen_6620, q_gen_6621, q_gen_6622},
Q_f={q_gen_6607},
Delta=
{
<cons>(q_gen_6621, q_gen_6620) -> q_gen_6620
<nil>() -> q_gen_6620
<s>(q_gen_6621) -> q_gen_6621
<z>() -> q_gen_6621
<cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6609
<nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6609
<nil, nil>() -> q_gen_6609
<s, s>(q_gen_6610) -> q_gen_6610
<s, z>(q_gen_6621) -> q_gen_6610
<z, s>(q_gen_6621) -> q_gen_6610
<z, z>() -> q_gen_6610
<cons, cons, cons>(q_gen_6622, q_gen_6607) -> q_gen_6607
<cons, nil, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, cons, cons>(q_gen_6610, q_gen_6609) -> q_gen_6607
<nil, nil, cons>(q_gen_6621, q_gen_6620) -> q_gen_6607
<nil, nil, nil>() -> q_gen_6607
<s, s, s>(q_gen_6622) -> q_gen_6622
<s, s, z>(q_gen_6610) -> q_gen_6622
<s, z, s>(q_gen_6610) -> q_gen_6622
<s, z, z>(q_gen_6621) -> q_gen_6622
<z, s, z>(q_gen_6621) -> q_gen_6622
<z, z, s>(q_gen_6621) -> q_gen_6622
<z, z, z>() -> q_gen_6622
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  not_null -> 
{{{
Q={q_gen_6604, q_gen_6605, q_gen_6606},
Q_f={q_gen_6604},
Delta=
{
<cons>(q_gen_6606, q_gen_6604) -> q_gen_6604
<cons>(q_gen_6606, q_gen_6605) -> q_gen_6604
<nil>() -> q_gen_6605
<s>(q_gen_6606) -> q_gen_6606
<z>() -> q_gen_6606
}

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

}
--
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([l1, l2, _cz]) /\ not_null([l1])) -> not_null([_cz]) -> 14
(append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]) -> 37
(not_null([nil])) -> BOT -> 15
}
Sat witness: Found: ((append([t1, l2, _xy])) -> append([cons(h1, t1), l2, cons(h1, _xy)]), {
_xy -> cons(s(s(z)), cons(z, cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(s(s(z)), nil))  ;  t1 -> cons(s(z), nil)
})

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