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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)])}
(append([_iy, _jy, _ky]) /\ append([_iy, _jy, _ly])) -> eq_natlist([_ky, _ly])
)
(not_null, P:
{() -> not_null([cons(x, ll)])
(not_null([nil])) -> BOT}
)
}

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


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

Clause system for inference is:

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


Solving took 60.000028 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4737, q_gen_4738, q_gen_4739, q_gen_4743, q_gen_4744, q_gen_4745, q_gen_4746, q_gen_4747, q_gen_4748, q_gen_4749, q_gen_4750, q_gen_4751, q_gen_4752, q_gen_4753, q_gen_4754, q_gen_4755, q_gen_4756, q_gen_4757, q_gen_4758, q_gen_4759, q_gen_4760, q_gen_4761, q_gen_4762, q_gen_4763, q_gen_4764, q_gen_4765, q_gen_4766, q_gen_4767, q_gen_4768, q_gen_4769, q_gen_4770, q_gen_4771, q_gen_4772, q_gen_4773, q_gen_4774, q_gen_4775, q_gen_4776, q_gen_4777, q_gen_4778, q_gen_4779, q_gen_4780, q_gen_4781, q_gen_4782, q_gen_4783, q_gen_4784, q_gen_4785, q_gen_4786, q_gen_4787, q_gen_4788, q_gen_4789, q_gen_4790, q_gen_4791, q_gen_4792, q_gen_4793, q_gen_4794, q_gen_4795, q_gen_4796, q_gen_4797, q_gen_4798, q_gen_4799, q_gen_4800, q_gen_4801, q_gen_4802, q_gen_4803, q_gen_4804, q_gen_4805},
Q_f={},
Delta=
{
<nil>() -> q_gen_4749
<z>() -> q_gen_4750
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4757
<s>(q_gen_4750) -> q_gen_4763
<s>(q_gen_4763) -> q_gen_4785
<nil, nil>() -> q_gen_4738
<z, z>() -> q_gen_4739
<cons, cons>(q_gen_4745, q_gen_4738) -> q_gen_4744
<s, s>(q_gen_4739) -> q_gen_4745
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4753
<cons, cons>(q_gen_4745, q_gen_4753) -> q_gen_4770
<nil, cons>(q_gen_4763, q_gen_4757) -> q_gen_4773
<s, z>(q_gen_4750) -> q_gen_4774
<z, s>(q_gen_4750) -> q_gen_4790
<nil, nil, nil>() -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4737
<nil, cons, cons>(q_gen_4745, q_gen_4744) -> q_gen_4743
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4746
<cons, cons, cons>(q_gen_4751, q_gen_4748) -> q_gen_4747
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4748
<z, z, z>() -> q_gen_4751
<cons, nil, cons>(q_gen_4739, q_gen_4753) -> q_gen_4752
<nil, cons, cons>(q_gen_4739, q_gen_4753) -> q_gen_4754
<cons, cons, cons>(q_gen_4751, q_gen_4756) -> q_gen_4755
<nil, nil, cons>(q_gen_4750, q_gen_4757) -> q_gen_4756
<cons, cons, cons>(q_gen_4759, q_gen_4756) -> q_gen_4758
<s, z, s>(q_gen_4739) -> q_gen_4759
<nil, cons, cons>(q_gen_4745, q_gen_4753) -> q_gen_4760
<cons, cons, cons>(q_gen_4764, q_gen_4762) -> q_gen_4761
<nil, nil, cons>(q_gen_4763, q_gen_4757) -> q_gen_4762
<s, s, s>(q_gen_4751) -> q_gen_4764
<cons, cons, cons>(q_gen_4764, q_gen_4736) -> q_gen_4765
<cons, cons, cons>(q_gen_4768, q_gen_4767) -> q_gen_4766
<cons, nil, cons>(q_gen_4745, q_gen_4738) -> q_gen_4767
<z, s, z>(q_gen_4750) -> q_gen_4768
<nil, cons, cons>(q_gen_4739, q_gen_4770) -> q_gen_4769
<cons, cons, cons>(q_gen_4759, q_gen_4772) -> q_gen_4771
<nil, cons, cons>(q_gen_4774, q_gen_4773) -> q_gen_4772
<cons, cons, cons>(q_gen_4777, q_gen_4776) -> q_gen_4775
<cons, cons, cons>(q_gen_4768, q_gen_4736) -> q_gen_4776
<s, z, s>(q_gen_4774) -> q_gen_4777
<cons, cons, cons>(q_gen_4759, q_gen_4779) -> q_gen_4778
<cons, cons, cons>(q_gen_4780, q_gen_4737) -> q_gen_4779
<s, s, s>(q_gen_4781) -> q_gen_4780
<s, z, z>(q_gen_4750) -> q_gen_4781
<cons, cons, cons>(q_gen_4777, q_gen_4783) -> q_gen_4782
<cons, cons, cons>(q_gen_4784, q_gen_4736) -> q_gen_4783
<z, s, z>(q_gen_4785) -> q_gen_4784
<cons, cons, cons>(q_gen_4759, q_gen_4787) -> q_gen_4786
<cons, cons, cons>(q_gen_4788, q_gen_4737) -> q_gen_4787
<s, s, s>(q_gen_4789) -> q_gen_4788
<s, s, z>(q_gen_4790) -> q_gen_4789
<cons, cons, cons>(q_gen_4781, q_gen_4792) -> q_gen_4791
<cons, cons, cons>(q_gen_4795, q_gen_4793) -> q_gen_4792
<cons, cons, cons>(q_gen_4795, q_gen_4794) -> q_gen_4793
<nil, cons, cons>(q_gen_4774, q_gen_4738) -> q_gen_4794
<s, z, s>(q_gen_4790) -> q_gen_4795
<cons, cons, cons>(q_gen_4759, q_gen_4797) -> q_gen_4796
<cons, cons, cons>(q_gen_4781, q_gen_4798) -> q_gen_4797
<cons, cons, cons>(q_gen_4795, q_gen_4799) -> q_gen_4798
<cons, cons, cons>(q_gen_4800, q_gen_4748) -> q_gen_4799
<s, s, s>(q_gen_4801) -> q_gen_4800
<z, z, s>(q_gen_4750) -> q_gen_4801
<cons, cons, cons>(q_gen_4801, q_gen_4794) -> q_gen_4802
<cons, cons, cons>(q_gen_4751, q_gen_4804) -> q_gen_4803
<cons, cons, cons>(q_gen_4805, q_gen_4748) -> q_gen_4804
<z, s, s>(q_gen_4739) -> q_gen_4805
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  not_null -> 
{{{
Q={q_gen_4733, q_gen_4734, q_gen_4735, q_gen_4740, q_gen_4741, q_gen_4742},
Q_f={},
Delta=
{
<cons>(q_gen_4735, q_gen_4734) -> q_gen_4733
<nil>() -> q_gen_4734
<z>() -> q_gen_4735
<cons>(q_gen_4735, q_gen_4741) -> q_gen_4740
<cons>(q_gen_4742, q_gen_4734) -> q_gen_4741
<s>(q_gen_4735) -> q_gen_4742
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.005595 s (model generation: 0.005027,  model checking: 0.000568):

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

}

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

}

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

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

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

-------------------------------------------
Step 1, which took 0.005305 s (model generation: 0.004915,  model checking: 0.000390):

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

}

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

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

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

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

-------------------------------------------
Step 2, which took 0.004963 s (model generation: 0.004930,  model checking: 0.000033):

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

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

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

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

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

})

-------------------------------------------
Step 3, which took 0.004862 s (model generation: 0.004475,  model checking: 0.000387):

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

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 3
(append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 1
(append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 4
(not_null([nil])) -> BOT -> 4
}
Sat witness: Found: ((append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]), {
_hy -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 4, which took 0.006410 s (model generation: 0.006199,  model checking: 0.000211):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739},
Q_f={q_gen_4736},
Delta=
{
<nil, nil>() -> q_gen_4738
<z, z>() -> q_gen_4739
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> not_null([cons(x, ll)]) -> 6
(append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 2
(append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 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.007473 s (model generation: 0.006739,  model checking: 0.000734):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739},
Q_f={q_gen_4736},
Delta=
{
<nil, nil>() -> q_gen_4738
<z, z>() -> q_gen_4739
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
}

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

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> not_null([cons(x, ll)]) -> 6
(append([l1, l2, _my]) /\ not_null([l1])) -> not_null([_my]) -> 3
(append([t1, l2, _hy])) -> append([cons(h1, t1), l2, cons(h1, _hy)]) -> 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.007670 s (model generation: 0.005276,  model checking: 0.002394):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739},
Q_f={q_gen_4736},
Delta=
{
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
}

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

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

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

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

-------------------------------------------
Step 7, which took 0.007890 s (model generation: 0.006373,  model checking: 0.001517):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<nil>() -> q_gen_4749
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 8, which took 0.007382 s (model generation: 0.005781,  model checking: 0.001601):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<nil>() -> q_gen_4749
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 9, which took 0.009551 s (model generation: 0.007161,  model checking: 0.002390):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 10, which took 0.011379 s (model generation: 0.006743,  model checking: 0.004636):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, z, s>(q_gen_4739) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 11, which took 0.013313 s (model generation: 0.008238,  model checking: 0.005075):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<s>(q_gen_4750) -> q_gen_4750
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, s, s>(q_gen_4751) -> q_gen_4751
<s, z, s>(q_gen_4739) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 12, which took 0.020116 s (model generation: 0.010941,  model checking: 0.009175):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<s>(q_gen_4750) -> q_gen_4750
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, s, s>(q_gen_4751) -> q_gen_4751
<s, z, s>(q_gen_4739) -> q_gen_4751
<z, s, z>(q_gen_4750) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 13, which took 0.028604 s (model generation: 0.012911,  model checking: 0.015693):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<s>(q_gen_4750) -> q_gen_4750
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<s, z>(q_gen_4750) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, s, s>(q_gen_4751) -> q_gen_4751
<s, z, s>(q_gen_4739) -> q_gen_4751
<z, s, z>(q_gen_4750) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 14, which took 0.035064 s (model generation: 0.017108,  model checking: 0.017956):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<s>(q_gen_4750) -> q_gen_4750
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<s, z>(q_gen_4750) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, s, s>(q_gen_4751) -> q_gen_4751
<s, z, s>(q_gen_4739) -> q_gen_4751
<s, z, z>(q_gen_4750) -> q_gen_4751
<z, s, z>(q_gen_4750) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 15, which took 0.052941 s (model generation: 0.022896,  model checking: 0.030045):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<s>(q_gen_4750) -> q_gen_4750
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<s, z>(q_gen_4750) -> q_gen_4739
<z, s>(q_gen_4750) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, s, s>(q_gen_4751) -> q_gen_4751
<s, s, z>(q_gen_4739) -> q_gen_4751
<s, z, s>(q_gen_4739) -> q_gen_4751
<s, z, z>(q_gen_4750) -> q_gen_4751
<z, s, z>(q_gen_4750) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

-------------------------------------------
Step 16, which took 0.064854 s (model generation: 0.047249,  model checking: 0.017605):

Model:
|_
{
append -> 
{{{
Q={q_gen_4736, q_gen_4738, q_gen_4739, q_gen_4749, q_gen_4750, q_gen_4751},
Q_f={q_gen_4736},
Delta=
{
<cons>(q_gen_4750, q_gen_4749) -> q_gen_4749
<nil>() -> q_gen_4749
<s>(q_gen_4750) -> q_gen_4750
<z>() -> q_gen_4750
<cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4738
<nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4738
<nil, nil>() -> q_gen_4738
<s, s>(q_gen_4739) -> q_gen_4739
<s, z>(q_gen_4750) -> q_gen_4739
<z, s>(q_gen_4750) -> q_gen_4739
<z, z>() -> q_gen_4739
<cons, cons, cons>(q_gen_4751, q_gen_4736) -> q_gen_4736
<cons, nil, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, cons, cons>(q_gen_4739, q_gen_4738) -> q_gen_4736
<nil, nil, cons>(q_gen_4750, q_gen_4749) -> q_gen_4736
<nil, nil, nil>() -> q_gen_4736
<s, s, s>(q_gen_4751) -> q_gen_4751
<s, s, z>(q_gen_4739) -> q_gen_4751
<s, z, s>(q_gen_4739) -> q_gen_4751
<s, z, z>(q_gen_4750) -> q_gen_4751
<z, s, z>(q_gen_4750) -> q_gen_4751
<z, z, s>(q_gen_4750) -> q_gen_4751
<z, z, z>() -> q_gen_4751
}

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

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

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

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

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