Solving ../../benchmarks/true/append_not_null2.smt2...

Inference procedure has parameters:
Ice fuel: 200
Timeout: 30s
Convolution: complete


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 30.076396 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_655, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_663, q_gen_664, q_gen_665, q_gen_666, q_gen_667, q_gen_668, q_gen_669, q_gen_670, q_gen_671, q_gen_672, q_gen_673, q_gen_674, q_gen_675, q_gen_676, q_gen_677, q_gen_678, q_gen_679, q_gen_680, q_gen_681, q_gen_682, q_gen_683, q_gen_684, q_gen_685, q_gen_686, q_gen_687, q_gen_688, q_gen_689, q_gen_690, q_gen_691, q_gen_692, q_gen_693, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700, q_gen_701, q_gen_702, q_gen_703, q_gen_704, q_gen_705, q_gen_706, q_gen_707, q_gen_708, q_gen_709, q_gen_710, q_gen_711, q_gen_712, q_gen_713, q_gen_714, q_gen_715, q_gen_716, q_gen_717, q_gen_718, q_gen_719, q_gen_720, q_gen_721, q_gen_722, q_gen_723, q_gen_724, q_gen_725, q_gen_726, q_gen_727, q_gen_728, q_gen_729, q_gen_730, q_gen_731, q_gen_732, q_gen_733, q_gen_734, q_gen_735, q_gen_736, q_gen_737, q_gen_738, q_gen_739, q_gen_740, q_gen_741, q_gen_742, q_gen_743, q_gen_744, q_gen_745, q_gen_746, q_gen_747, q_gen_748, q_gen_749, q_gen_750, q_gen_751, q_gen_752, q_gen_753, q_gen_754, q_gen_755, q_gen_756, q_gen_757, q_gen_758, q_gen_759, q_gen_760, q_gen_761, q_gen_762, q_gen_763, q_gen_764, q_gen_765, q_gen_766, q_gen_767, q_gen_768, q_gen_769, q_gen_770, q_gen_771, q_gen_772, q_gen_773, q_gen_774, q_gen_775, q_gen_776, q_gen_777, q_gen_778, q_gen_779},
Q_f={},
Delta=
{
<z>() -> q_gen_665
<s>(q_gen_665) -> q_gen_670
<nil>() -> q_gen_676
<cons>(q_gen_665, q_gen_676) -> q_gen_684
<nil, nil>() -> q_gen_656
<nil, z>() -> q_gen_657
<z, nil>() -> q_gen_658
<z, z>() -> q_gen_659
<nil, s>(q_gen_665) -> q_gen_664
<s, nil>(q_gen_665) -> q_gen_666
<s, s>(q_gen_659) -> q_gen_667
<nil, s>(q_gen_670) -> q_gen_669
<s, nil>(q_gen_670) -> q_gen_671
<s, s>(q_gen_667) -> q_gen_672
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_674
<cons, z>(q_gen_665, q_gen_676) -> q_gen_675
<z, cons>(q_gen_665, q_gen_676) -> q_gen_677
<cons, s>(q_gen_659, q_gen_657) -> q_gen_679
<s, cons>(q_gen_659, q_gen_658) -> q_gen_680
<cons, cons>(q_gen_659, q_gen_677, q_gen_675, q_gen_674) -> q_gen_682
<cons, z>(q_gen_665, q_gen_684) -> q_gen_683
<z, cons>(q_gen_665, q_gen_684) -> q_gen_685
<cons, s>(q_gen_688, q_gen_664) -> q_gen_687
<z, s>(q_gen_665) -> q_gen_688
<s, cons>(q_gen_690, q_gen_666) -> q_gen_689
<s, z>(q_gen_665) -> q_gen_690
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_702
<s, z>(q_gen_670) -> q_gen_731
<s, s>(q_gen_690) -> q_gen_751
<nil, nil, nil>() -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_655
<nil, cons, cons>(q_gen_667, q_gen_666, q_gen_664, q_gen_656) -> q_gen_663
<cons, nil, cons>(q_gen_672, q_gen_671, q_gen_669, q_gen_656) -> q_gen_668
<nil, cons, cons>(q_gen_659, q_gen_677, q_gen_675, q_gen_674) -> q_gen_673
<cons, nil, cons>(q_gen_667, q_gen_680, q_gen_679, q_gen_674) -> q_gen_678
<nil, cons, cons>(q_gen_659, q_gen_685, q_gen_683, q_gen_682) -> q_gen_681
<cons, nil, cons>(q_gen_672, q_gen_689, q_gen_687, q_gen_674) -> q_gen_686
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_691
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_693) -> q_gen_692
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_693
<nil, nil, z>() -> q_gen_694
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, z, z>() -> q_gen_696
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<z, nil, z>() -> q_gen_698
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, z>() -> q_gen_700
<cons, nil, cons>(q_gen_659, q_gen_677, q_gen_657, q_gen_702) -> q_gen_701
<nil, cons, cons>(q_gen_690, q_gen_666, q_gen_657, q_gen_656) -> q_gen_703
<cons, cons, cons>(q_gen_713, q_gen_710, q_gen_709, q_gen_708, q_gen_707, q_gen_706, q_gen_705, q_gen_693) -> q_gen_704
<nil, nil, s>(q_gen_670) -> q_gen_705
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_706
<nil, s, s>(q_gen_688) -> q_gen_707
<s, nil, cons>(q_gen_690, q_gen_666) -> q_gen_708
<s, nil, s>(q_gen_667) -> q_gen_709
<s, s, cons>(q_gen_712, q_gen_711) -> q_gen_710
<s, z, nil>(q_gen_665) -> q_gen_711
<s, z, z>(q_gen_665) -> q_gen_712
<s, s, s>(q_gen_714) -> q_gen_713
<s, z, s>(q_gen_659) -> q_gen_714
<cons, cons, cons>(q_gen_714, q_gen_720, q_gen_719, q_gen_718, q_gen_717, q_gen_695, q_gen_716, q_gen_693) -> q_gen_715
<nil, nil, s>(q_gen_665) -> q_gen_716
<nil, z, s>(q_gen_665) -> q_gen_717
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_718
<s, nil, s>(q_gen_659) -> q_gen_719
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_720
<cons, cons, cons>(q_gen_725, q_gen_723, q_gen_719, q_gen_718, q_gen_722, q_gen_706, q_gen_716, q_gen_693) -> q_gen_721
<nil, s, s>(q_gen_659) -> q_gen_722
<s, s, cons>(q_gen_700, q_gen_724) -> q_gen_723
<z, z, nil>() -> q_gen_724
<s, s, s>(q_gen_700) -> q_gen_725
<cons, cons, cons>(q_gen_729, q_gen_728, q_gen_698, q_gen_697, q_gen_727, q_gen_706, q_gen_694, q_gen_693) -> q_gen_726
<nil, s, z>(q_gen_665) -> q_gen_727
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_728
<z, s, z>(q_gen_665) -> q_gen_729
<nil, cons, cons>(q_gen_731, q_gen_671, q_gen_657, q_gen_656) -> q_gen_730
<cons, cons, cons>(q_gen_737, q_gen_735, q_gen_719, q_gen_718, q_gen_734, q_gen_733, q_gen_716, q_gen_693) -> q_gen_732
<nil, s, cons>(q_gen_690, q_gen_666) -> q_gen_733
<nil, s, s>(q_gen_690) -> q_gen_734
<s, s, cons>(q_gen_729, q_gen_736) -> q_gen_735
<z, s, nil>(q_gen_665) -> q_gen_736
<s, s, s>(q_gen_729) -> q_gen_737
<cons, cons, cons>(q_gen_743, q_gen_740, q_gen_709, q_gen_708, q_gen_739, q_gen_733, q_gen_705, q_gen_693) -> q_gen_738
<nil, s, s>(q_gen_667) -> q_gen_739
<s, s, cons>(q_gen_742, q_gen_741) -> q_gen_740
<s, s, nil>(q_gen_659) -> q_gen_741
<s, s, z>(q_gen_659) -> q_gen_742
<s, s, s>(q_gen_725) -> q_gen_743
<cons, cons, cons>(q_gen_725, q_gen_748, q_gen_719, q_gen_747, q_gen_722, q_gen_746, q_gen_716, q_gen_745) -> q_gen_744
<nil, nil, cons>(q_gen_670, q_gen_676) -> q_gen_745
<nil, s, cons>(q_gen_688, q_gen_658) -> q_gen_746
<s, nil, cons>(q_gen_688, q_gen_658) -> q_gen_747
<s, s, cons>(q_gen_749, q_gen_724) -> q_gen_748
<z, z, s>(q_gen_665) -> q_gen_749
<nil, cons, cons>(q_gen_751, q_gen_671, q_gen_664, q_gen_656) -> q_gen_750
<cons, cons, cons>(q_gen_737, q_gen_754, q_gen_719, q_gen_747, q_gen_734, q_gen_753, q_gen_716, q_gen_745) -> q_gen_752
<nil, s, cons>(q_gen_667, q_gen_666) -> q_gen_753
<s, s, cons>(q_gen_755, q_gen_736) -> q_gen_754
<z, s, s>(q_gen_659) -> q_gen_755
<cons, cons, cons>(q_gen_700, q_gen_762, q_gen_761, q_gen_760, q_gen_696, q_gen_759, q_gen_758, q_gen_757) -> q_gen_756
<nil, cons, cons>(q_gen_659, q_gen_677, q_gen_657, q_gen_702) -> q_gen_757
<nil, cons, z>(q_gen_665, q_gen_676) -> q_gen_758
<nil, z, cons>(q_gen_665, q_gen_684) -> q_gen_759
<z, cons, cons>(q_gen_659, q_gen_677, q_gen_657, q_gen_702) -> q_gen_760
<z, cons, z>(q_gen_665, q_gen_676) -> q_gen_761
<z, z, cons>(q_gen_665, q_gen_684) -> q_gen_762
<cons, cons, cons>(q_gen_700, q_gen_762, q_gen_698, q_gen_767, q_gen_766, q_gen_765, q_gen_764, q_gen_701) -> q_gen_763
<cons, nil, z>(q_gen_665, q_gen_676) -> q_gen_764
<cons, z, cons>(q_gen_659, q_gen_677, q_gen_657, q_gen_702) -> q_gen_765
<cons, z, z>(q_gen_665, q_gen_676) -> q_gen_766
<z, nil, cons>(q_gen_665, q_gen_684) -> q_gen_767
<cons, cons, cons>(q_gen_714, q_gen_772, q_gen_719, q_gen_771, q_gen_770, q_gen_765, q_gen_769, q_gen_701) -> q_gen_768
<cons, nil, s>(q_gen_659, q_gen_657) -> q_gen_769
<cons, z, s>(q_gen_659, q_gen_657) -> q_gen_770
<s, nil, cons>(q_gen_659, q_gen_677) -> q_gen_771
<s, z, cons>(q_gen_659, q_gen_677) -> q_gen_772
<cons, cons, cons>(q_gen_729, q_gen_776, q_gen_698, q_gen_767, q_gen_775, q_gen_774, q_gen_764, q_gen_701) -> q_gen_773
<cons, s, cons>(q_gen_700, q_gen_699, q_gen_696, q_gen_695) -> q_gen_774
<cons, s, z>(q_gen_659, q_gen_657) -> q_gen_775
<z, s, cons>(q_gen_659, q_gen_677) -> q_gen_776
<cons, cons, cons>(q_gen_725, q_gen_779, q_gen_719, q_gen_771, q_gen_778, q_gen_774, q_gen_769, q_gen_701) -> q_gen_777
<cons, s, s>(q_gen_700, q_gen_696) -> q_gen_778
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_779
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653, q_gen_660, q_gen_661, q_gen_662},
Q_f={},
Delta=
{
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<z>() -> q_gen_653
<cons>(q_gen_653, q_gen_661) -> q_gen_660
<cons>(q_gen_662, q_gen_652) -> q_gen_661
<s>(q_gen_653) -> q_gen_662
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.004308 s (model generation: 0.003916,  model checking: 0.000392):

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

}

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

}

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

}
--
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: Yes: (() -> not_null([cons(x, ll)]), {
ll -> nil  ;  x -> z
})

-------------------------------------------
Step 1, which took 0.003965 s (model generation: 0.003654,  model checking: 0.000311):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<nil>() -> q_gen_651
<z>() -> q_gen_653
}

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

}
--
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: Yes: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 2, which took 0.003541 s (model generation: 0.003534,  model checking: 0.000007):

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

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<nil>() -> q_gen_651
<z>() -> q_gen_653
}

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

}
--
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: Yes: ((not_null([nil])) -> BOT, {

})

-------------------------------------------
Step 3, which took 0.003883 s (model generation: 0.003434,  model checking: 0.000449):

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

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<z>() -> q_gen_653
}

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

}
--
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: Yes: ((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.004368 s (model generation: 0.004098,  model checking: 0.000270):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659},
Q_f={q_gen_654},
Delta=
{
<nil, nil>() -> q_gen_656
<nil, z>() -> q_gen_657
<z, nil>() -> q_gen_658
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<z>() -> q_gen_653
}

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

}
--
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: Yes: (() -> not_null([cons(x, ll)]), {
ll -> cons(s(z), nil)  ;  x -> z
})

-------------------------------------------
Step 5, which took 0.018643 s (model generation: 0.007133,  model checking: 0.011510):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659},
Q_f={q_gen_654},
Delta=
{
<nil, nil>() -> q_gen_656
<nil, z>() -> q_gen_657
<z, nil>() -> q_gen_658
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), nil)
})

-------------------------------------------
Step 6, which took 0.006665 s (model generation: 0.004815,  model checking: 0.001850):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665},
Q_f={q_gen_654},
Delta=
{
<z>() -> q_gen_665
<nil, nil>() -> q_gen_656
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, nil>(q_gen_665) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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: Yes: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> nil  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.030184 s (model generation: 0.006527,  model checking: 0.023657):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<nil, nil>() -> q_gen_656
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, nil>(q_gen_665) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 7  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 7  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 6  ;  (not_null([nil])) -> BOT -> 6
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 8, which took 0.008044 s (model generation: 0.004803,  model checking: 0.003241):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 7  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 10  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 7  ;  (not_null([nil])) -> BOT -> 7
}
Sat witness: Yes: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 9, which took 0.041024 s (model generation: 0.005018,  model checking: 0.036006):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 8  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 10  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 8  ;  (not_null([nil])) -> BOT -> 8
}
Sat witness: Yes: (() -> append([nil, l2, l2]), {
l2 -> cons(z, cons(z, cons(z, nil)))
})

-------------------------------------------
Step 10, which took 0.009775 s (model generation: 0.005859,  model checking: 0.003916):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 9  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 13  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 9  ;  (not_null([nil])) -> BOT -> 9
}
Sat witness: Yes: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 11, which took 0.010828 s (model generation: 0.006318,  model checking: 0.004510):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 10  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 16  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 10  ;  (not_null([nil])) -> BOT -> 10
}
Sat witness: Yes: ((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 12, which took 0.034263 s (model generation: 0.007144,  model checking: 0.027119):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, z>() -> q_gen_694
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, z, z>() -> q_gen_696
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<z, nil, z>() -> q_gen_698
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 11  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 19  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 11  ;  (not_null([nil])) -> BOT -> 11
}
Sat witness: Yes: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.614964 s (model generation: 0.007942,  model checking: 0.607022):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, z>() -> q_gen_694
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, z, z>() -> q_gen_696
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<z, nil, z>() -> q_gen_698
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 12  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 22  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 12  ;  (not_null([nil])) -> BOT -> 12
}
Sat witness: Yes: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> s(s(z))  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.158025 s (model generation: 0.010110,  model checking: 0.147915):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

}
--
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)]) -> 13  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 25  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 13  ;  (not_null([nil])) -> BOT -> 13
}
Sat witness: Yes: ((append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]), {
_gh -> cons(z, nil)  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.165597 s (model generation: 0.010505,  model checking: 0.155092):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 16, which took 0.204954 s (model generation: 0.011754,  model checking: 0.193200):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 17, which took 0.165092 s (model generation: 0.012534,  model checking: 0.152558):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 18, which took 0.376646 s (model generation: 0.014681,  model checking: 0.361965):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 19, which took 0.528746 s (model generation: 0.017420,  model checking: 0.511326):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 20, which took 0.540989 s (model generation: 0.019664,  model checking: 0.521325):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, s>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 21, which took 0.570048 s (model generation: 0.024195,  model checking: 0.545853):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, s>(q_gen_659) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, s>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 22, which took 1.617748 s (model generation: 0.034371,  model checking: 1.583377):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<nil, cons, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, cons, z>(q_gen_665, q_gen_676) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, s>(q_gen_659) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, s>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24  ;  () -> not_null([cons(x, ll)]) -> 21  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 49  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 21  ;  (not_null([nil])) -> BOT -> 21
}
Sat witness: Yes: ((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 -> cons(z, nil)
})

-------------------------------------------
Step 23, which took 1.472365 s (model generation: 0.037645,  model checking: 1.434720):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<cons, nil, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, cons, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<cons, z, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_695
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<cons, z, z>(q_gen_665, q_gen_676) -> q_gen_696
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, cons, z>(q_gen_665, q_gen_676) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, s>(q_gen_659) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, s>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25  ;  () -> not_null([cons(x, ll)]) -> 22  ;  (append([t1, l2, _gh])) -> append([cons(h1, t1), l2, cons(h1, _gh)]) -> 52  ;  (append([cons(i, l1), l2, _lh])) -> not_null([_lh]) -> 22  ;  (not_null([nil])) -> BOT -> 22
}
Sat witness: Yes: ((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 -> cons(z, nil)
})

-------------------------------------------
Step 24, which took 11.460214 s (model generation: 0.038104,  model checking: 11.422110):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<cons, nil, s>(q_gen_659, q_gen_657) -> q_gen_694
<cons, nil, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, cons, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<cons, z, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_695
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<cons, z, s>(q_gen_659, q_gen_657) -> q_gen_696
<cons, z, z>(q_gen_665, q_gen_676) -> q_gen_696
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, cons, z>(q_gen_665, q_gen_676) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, s>(q_gen_659) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, s>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

-------------------------------------------
Step 25, which took 11.436785 s (model generation: 0.041874,  model checking: 11.394911):

Model:
|_
{
append -> 
{{{
Q={q_gen_654, q_gen_656, q_gen_657, q_gen_658, q_gen_659, q_gen_665, q_gen_676, q_gen_694, q_gen_695, q_gen_696, q_gen_697, q_gen_698, q_gen_699, q_gen_700},
Q_f={q_gen_654},
Delta=
{
<s>(q_gen_665) -> q_gen_665
<z>() -> q_gen_665
<cons>(q_gen_665, q_gen_676) -> q_gen_676
<nil>() -> q_gen_676
<cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_656
<nil, cons>(q_gen_665, q_gen_676) -> q_gen_656
<nil, nil>() -> q_gen_656
<cons, s>(q_gen_659, q_gen_657) -> q_gen_657
<cons, z>(q_gen_665, q_gen_676) -> q_gen_657
<nil, s>(q_gen_665) -> q_gen_657
<nil, z>() -> q_gen_657
<s, cons>(q_gen_659, q_gen_658) -> q_gen_658
<s, nil>(q_gen_665) -> q_gen_658
<z, cons>(q_gen_665, q_gen_676) -> q_gen_658
<z, nil>() -> q_gen_658
<s, s>(q_gen_659) -> q_gen_659
<s, z>(q_gen_665) -> q_gen_659
<z, s>(q_gen_665) -> q_gen_659
<z, z>() -> q_gen_659
<cons, cons, cons>(q_gen_700, q_gen_699, q_gen_698, q_gen_697, q_gen_696, q_gen_695, q_gen_694, q_gen_654) -> q_gen_654
<cons, nil, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_654
<nil, nil, cons>(q_gen_665, q_gen_676) -> q_gen_654
<nil, nil, nil>() -> q_gen_654
<cons, nil, s>(q_gen_659, q_gen_657) -> q_gen_694
<cons, nil, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, cons, z>(q_gen_665, q_gen_676) -> q_gen_694
<nil, nil, s>(q_gen_665) -> q_gen_694
<nil, nil, z>() -> q_gen_694
<cons, s, cons>(q_gen_700, q_gen_699, q_gen_696, q_gen_695) -> q_gen_695
<cons, z, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_695
<nil, s, cons>(q_gen_659, q_gen_658) -> q_gen_695
<nil, z, cons>(q_gen_665, q_gen_676) -> q_gen_695
<cons, s, z>(q_gen_659, q_gen_657) -> q_gen_696
<cons, z, s>(q_gen_659, q_gen_657) -> q_gen_696
<cons, z, z>(q_gen_665, q_gen_676) -> q_gen_696
<nil, s, s>(q_gen_659) -> q_gen_696
<nil, s, z>(q_gen_665) -> q_gen_696
<nil, z, s>(q_gen_665) -> q_gen_696
<nil, z, z>() -> q_gen_696
<s, nil, cons>(q_gen_659, q_gen_658) -> q_gen_697
<z, cons, cons>(q_gen_659, q_gen_658, q_gen_657, q_gen_656) -> q_gen_697
<z, nil, cons>(q_gen_665, q_gen_676) -> q_gen_697
<s, nil, s>(q_gen_659) -> q_gen_698
<z, cons, z>(q_gen_665, q_gen_676) -> q_gen_698
<z, nil, z>() -> q_gen_698
<s, s, cons>(q_gen_700, q_gen_699) -> q_gen_699
<s, s, nil>(q_gen_659) -> q_gen_699
<s, z, cons>(q_gen_659, q_gen_658) -> q_gen_699
<s, z, nil>(q_gen_665) -> q_gen_699
<z, s, cons>(q_gen_659, q_gen_658) -> q_gen_699
<z, s, nil>(q_gen_665) -> q_gen_699
<z, z, cons>(q_gen_665, q_gen_676) -> q_gen_699
<z, z, nil>() -> q_gen_699
<s, s, s>(q_gen_700) -> q_gen_700
<s, s, z>(q_gen_659) -> q_gen_700
<s, z, s>(q_gen_659) -> q_gen_700
<s, z, z>(q_gen_665) -> q_gen_700
<z, s, s>(q_gen_659) -> q_gen_700
<z, s, z>(q_gen_665) -> q_gen_700
<z, z, s>(q_gen_665) -> q_gen_700
<z, z, z>() -> q_gen_700
}

Datatype: <natlist, natlist, natlist>
Convolution form: complete
}}}
  ;  not_null -> 
{{{
Q={q_gen_651, q_gen_652, q_gen_653},
Q_f={q_gen_651},
Delta=
{
<cons>(q_gen_653, q_gen_651) -> q_gen_651
<cons>(q_gen_653, q_gen_652) -> q_gen_651
<nil>() -> q_gen_652
<s>(q_gen_653) -> q_gen_653
<z>() -> q_gen_653
}

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

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

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

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