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, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)])}
(append([_tb, _ub, _vb]) /\ append([_tb, _ub, _wb])) -> eq_natlist([_vb, _wb])
)
(leq, P:
{() -> leq([z, s(nn2)])
() -> leq([z, z])
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)])
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2])
(leq([s(nn1), z])) -> BOT}
)
(length, F:
{() -> length([nil, z])
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)])}
(length([_yb, _ac]) /\ length([_yb, _zb])) -> eq_nat([_zb, _ac])
)
}

properties:
{(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc])}


over-approximation: {append, length}
under-approximation: {leq}

Clause system for inference is:

{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 0
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 0
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 0
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 0
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 0
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 0
(leq([s(nn1), z])) -> BOT -> 0
}


Solving took 60.000098 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_467, q_gen_468, q_gen_469, q_gen_472, q_gen_473, q_gen_474, q_gen_477, q_gen_478, q_gen_479, q_gen_480, q_gen_481, q_gen_482, q_gen_483, q_gen_484, q_gen_485, q_gen_486, q_gen_487, q_gen_488, q_gen_489, q_gen_490, q_gen_491, q_gen_492, q_gen_493, q_gen_494, q_gen_495, q_gen_496, q_gen_497, q_gen_498, q_gen_499, q_gen_500, q_gen_501, q_gen_502, q_gen_503, q_gen_504, q_gen_505, q_gen_506, q_gen_507, q_gen_508, q_gen_509, q_gen_510, q_gen_511, q_gen_512, q_gen_513, q_gen_514, q_gen_515, q_gen_516, q_gen_517, q_gen_518, q_gen_519, q_gen_520, q_gen_521, q_gen_522, q_gen_523, q_gen_524, q_gen_525, q_gen_526, q_gen_527, q_gen_528, q_gen_529, q_gen_530, q_gen_531, q_gen_532, q_gen_533, q_gen_534, q_gen_535, q_gen_536, q_gen_537, q_gen_538, q_gen_539, q_gen_540, q_gen_541, q_gen_542, q_gen_543, q_gen_544, q_gen_545, q_gen_546, q_gen_547},
Q_f={},
Delta=
{
<nil>() -> q_gen_480
<z>() -> q_gen_481
<cons>(q_gen_481, q_gen_480) -> q_gen_488
<s>(q_gen_481) -> q_gen_494
<s>(q_gen_518) -> q_gen_517
<s>(q_gen_494) -> q_gen_518
<nil, nil>() -> q_gen_468
<z, z>() -> q_gen_469
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_473
<s, s>(q_gen_469) -> q_gen_474
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_484
<cons, cons>(q_gen_474, q_gen_484) -> q_gen_501
<nil, cons>(q_gen_494, q_gen_488) -> q_gen_504
<s, z>(q_gen_481) -> q_gen_505
<s, s>(q_gen_505) -> q_gen_520
<z, s>(q_gen_481) -> q_gen_527
<s, z>(q_gen_494) -> q_gen_542
<nil, nil, nil>() -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_467
<nil, cons, cons>(q_gen_474, q_gen_473) -> q_gen_472
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_477
<cons, cons, cons>(q_gen_482, q_gen_479) -> q_gen_478
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_479
<z, z, z>() -> q_gen_482
<cons, nil, cons>(q_gen_469, q_gen_484) -> q_gen_483
<nil, cons, cons>(q_gen_469, q_gen_484) -> q_gen_485
<cons, cons, cons>(q_gen_482, q_gen_487) -> q_gen_486
<nil, nil, cons>(q_gen_481, q_gen_488) -> q_gen_487
<cons, cons, cons>(q_gen_490, q_gen_487) -> q_gen_489
<s, z, s>(q_gen_469) -> q_gen_490
<nil, cons, cons>(q_gen_474, q_gen_468) -> q_gen_491
<cons, cons, cons>(q_gen_495, q_gen_493) -> q_gen_492
<nil, nil, cons>(q_gen_494, q_gen_480) -> q_gen_493
<s, s, s>(q_gen_482) -> q_gen_495
<cons, cons, cons>(q_gen_495, q_gen_463) -> q_gen_496
<cons, cons, cons>(q_gen_499, q_gen_498) -> q_gen_497
<cons, nil, cons>(q_gen_474, q_gen_468) -> q_gen_498
<z, s, z>(q_gen_481) -> q_gen_499
<nil, cons, cons>(q_gen_469, q_gen_501) -> q_gen_500
<cons, cons, cons>(q_gen_490, q_gen_503) -> q_gen_502
<nil, cons, cons>(q_gen_505, q_gen_504) -> q_gen_503
<cons, cons, cons>(q_gen_508, q_gen_507) -> q_gen_506
<nil, cons, cons>(q_gen_505, q_gen_468) -> q_gen_507
<s, z, s>(q_gen_505) -> q_gen_508
<cons, cons, cons>(q_gen_490, q_gen_510) -> q_gen_509
<cons, cons, cons>(q_gen_511, q_gen_479) -> q_gen_510
<s, s, s>(q_gen_512) -> q_gen_511
<s, z, z>(q_gen_481) -> q_gen_512
<cons, cons, cons>(q_gen_519, q_gen_514) -> q_gen_513
<cons, cons, cons>(q_gen_516, q_gen_515) -> q_gen_514
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_515
<z, s, z>(q_gen_517) -> q_gen_516
<s, z, s>(q_gen_520) -> q_gen_519
<cons, cons, cons>(q_gen_490, q_gen_522) -> q_gen_521
<cons, cons, cons>(q_gen_524, q_gen_523) -> q_gen_522
<cons, cons, cons>(q_gen_482, q_gen_467) -> q_gen_523
<s, s, s>(q_gen_525) -> q_gen_524
<s, s, s>(q_gen_526) -> q_gen_525
<s, s, z>(q_gen_527) -> q_gen_526
<cons, cons, cons>(q_gen_512, q_gen_529) -> q_gen_528
<cons, cons, cons>(q_gen_532, q_gen_530) -> q_gen_529
<cons, cons, cons>(q_gen_532, q_gen_531) -> q_gen_530
<nil, cons, cons>(q_gen_505, q_gen_484) -> q_gen_531
<s, z, s>(q_gen_527) -> q_gen_532
<cons, cons, cons>(q_gen_490, q_gen_534) -> q_gen_533
<cons, cons, cons>(q_gen_512, q_gen_535) -> q_gen_534
<cons, cons, cons>(q_gen_532, q_gen_536) -> q_gen_535
<cons, cons, cons>(q_gen_537, q_gen_487) -> q_gen_536
<s, s, s>(q_gen_538) -> q_gen_537
<z, z, s>(q_gen_481) -> q_gen_538
<cons, cons, cons>(q_gen_532, q_gen_540) -> q_gen_539
<cons, cons, cons>(q_gen_532, q_gen_541) -> q_gen_540
<nil, cons, cons>(q_gen_542, q_gen_468) -> q_gen_541
<cons, cons, cons>(q_gen_482, q_gen_544) -> q_gen_543
<cons, cons, cons>(q_gen_532, q_gen_545) -> q_gen_544
<cons, cons, cons>(q_gen_546, q_gen_479) -> q_gen_545
<s, s, s>(q_gen_547) -> q_gen_546
<z, s, s>(q_gen_469) -> q_gen_547
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_465, q_gen_466, q_gen_475, q_gen_476},
Q_f={},
Delta=
{
<z>() -> q_gen_466
<s>(q_gen_466) -> q_gen_476
<nil, z>() -> q_gen_462
<cons, s>(q_gen_466, q_gen_462) -> q_gen_465
<cons, s>(q_gen_476, q_gen_462) -> q_gen_475
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_460, q_gen_461, q_gen_464, q_gen_470, q_gen_471},
Q_f={},
Delta=
{
<z>() -> q_gen_461
<s>(q_gen_461) -> q_gen_471
<z, z>() -> q_gen_459
<z, s>(q_gen_461) -> q_gen_460
<s, s>(q_gen_459) -> q_gen_464
<z, s>(q_gen_471) -> q_gen_470
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.030316 s (model generation: 0.005342,  model checking: 0.024974):

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

}

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

}

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

}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 0
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, z]), {

})

-------------------------------------------
Step 1, which took 0.004936 s (model generation: 0.004734,  model checking: 0.000202):

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

}

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

}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459},
Q_f={q_gen_459},
Delta=
{
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 0
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> z
})

-------------------------------------------
Step 2, which took 0.006093 s (model generation: 0.005954,  model checking: 0.000139):

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

}

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

}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<z>() -> q_gen_461
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 0
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> length([nil, z]), {

})

-------------------------------------------
Step 3, which took 0.004384 s (model generation: 0.003953,  model checking: 0.000431):

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

}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462},
Q_f={q_gen_462},
Delta=
{
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<z>() -> q_gen_461
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 1
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 1
(leq([s(nn1), z])) -> BOT -> 1
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> nil
})

-------------------------------------------
Step 4, which took 0.005555 s (model generation: 0.005202,  model checking: 0.000353):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462},
Q_f={q_gen_462},
Delta=
{
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<z>() -> q_gen_461
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 1
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]), {
nn1 -> z  ;  nn2 -> z
})

-------------------------------------------
Step 5, which took 0.005736 s (model generation: 0.005481,  model checking: 0.000255):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462},
Q_f={q_gen_462},
Delta=
{
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 1
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((length([ll, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> z  ;  ll -> nil  ;  x -> z
})

-------------------------------------------
Step 6, which took 0.005707 s (model generation: 0.004691,  model checking: 0.001016):

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

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 3
() -> leq([z, z]) -> 3
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 1
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 2
(leq([s(nn1), z])) -> BOT -> 2
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.005471 s (model generation: 0.004955,  model checking: 0.000516):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469},
Q_f={q_gen_463},
Delta=
{
<nil, nil>() -> q_gen_468
<z, z>() -> q_gen_469
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 3
() -> length([nil, z]) -> 3
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 2
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 3
(leq([s(nn1), z])) -> BOT -> 3
}
Sat witness: Found: (() -> leq([z, s(nn2)]), {
nn2 -> s(z)
})

-------------------------------------------
Step 8, which took 0.006451 s (model generation: 0.005810,  model checking: 0.000641):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469},
Q_f={q_gen_463},
Delta=
{
<nil, nil>() -> q_gen_468
<z, z>() -> q_gen_469
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 3
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 4
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 4
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 4
(leq([s(nn1), z])) -> BOT -> 4
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(s(z), cons(z, nil))
})

-------------------------------------------
Step 9, which took 0.006376 s (model generation: 0.005326,  model checking: 0.001050):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469},
Q_f={q_gen_463},
Delta=
{
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 4
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 4
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((length([ll, _xb])) -> length([cons(x, ll), s(_xb)]), {
_xb -> z  ;  ll -> nil  ;  x -> s(z)
})

-------------------------------------------
Step 10, which took 0.008329 s (model generation: 0.006866,  model checking: 0.001463):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469},
Q_f={q_gen_463},
Delta=
{
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 6
() -> length([nil, z]) -> 4
() -> leq([z, s(nn2)]) -> 6
() -> leq([z, z]) -> 4
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 4
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 7
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 7
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 5
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 5
(leq([s(nn1), z])) -> BOT -> 5
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.008748 s (model generation: 0.007051,  model checking: 0.001697):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<nil>() -> q_gen_480
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 5
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 5
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 5
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 10
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 8
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 6
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 6
(leq([s(nn1), z])) -> BOT -> 6
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 12, which took 0.008799 s (model generation: 0.006437,  model checking: 0.002362):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<nil>() -> q_gen_480
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 6
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 6
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 6
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 13
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 9
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 7
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 7
(leq([s(nn1), z])) -> BOT -> 7
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.009440 s (model generation: 0.007065,  model checking: 0.002375):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 9
() -> leq([z, z]) -> 7
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 7
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 16
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 10
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 8
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 14, which took 0.027479 s (model generation: 0.008956,  model checking: 0.018523):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, z, s>(q_gen_469) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 8
() -> leq([z, s(nn2)]) -> 10
() -> leq([z, z]) -> 8
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 8
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 19
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 11
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 9
(leq([s(nn1), z])) -> BOT -> 9
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(z), nil)  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 15, which took 0.016517 s (model generation: 0.010138,  model checking: 0.006379):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<s>(q_gen_481) -> q_gen_481
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, s, s>(q_gen_482) -> q_gen_482
<s, z, s>(q_gen_469) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 9
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 9
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 9
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 22
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 12
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 10
(leq([s(nn1), z])) -> BOT -> 10
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(z), nil)  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 16, which took 0.093894 s (model generation: 0.085504,  model checking: 0.008390):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<s>(q_gen_481) -> q_gen_481
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, s, s>(q_gen_482) -> q_gen_482
<s, z, s>(q_gen_469) -> q_gen_482
<z, s, z>(q_gen_481) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> length([nil, z]) -> 10
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 10
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 10
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 25
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(s(z), cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> nil
})

-------------------------------------------
Step 17, which took 0.031242 s (model generation: 0.014180,  model checking: 0.017062):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<s>(q_gen_481) -> q_gen_481
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_481) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, s, s>(q_gen_482) -> q_gen_482
<s, z, s>(q_gen_469) -> q_gen_482
<z, s, z>(q_gen_481) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 11
() -> leq([z, s(nn2)]) -> 13
() -> leq([z, z]) -> 11
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 11
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 28
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 14
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 18, which took 0.031371 s (model generation: 0.017654,  model checking: 0.013717):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<s>(q_gen_481) -> q_gen_481
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_481) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, s, s>(q_gen_482) -> q_gen_482
<s, z, s>(q_gen_469) -> q_gen_482
<s, z, z>(q_gen_481) -> q_gen_482
<z, s, z>(q_gen_481) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 12
() -> leq([z, s(nn2)]) -> 14
() -> leq([z, z]) -> 12
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 12
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 31
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 15
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(s(z)), cons(z, cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(s(s(s(z)))), cons(z, nil)))  ;  t1 -> cons(s(s(s(z))), cons(z, cons(z, nil)))
})

-------------------------------------------
Step 19, which took 0.058497 s (model generation: 0.030808,  model checking: 0.027689):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<s>(q_gen_481) -> q_gen_481
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_481) -> q_gen_469
<z, s>(q_gen_481) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, s, s>(q_gen_482) -> q_gen_482
<s, s, z>(q_gen_469) -> q_gen_482
<s, z, s>(q_gen_469) -> q_gen_482
<s, z, z>(q_gen_481) -> q_gen_482
<z, s, z>(q_gen_481) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 13
() -> leq([z, s(nn2)]) -> 15
() -> leq([z, z]) -> 13
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 13
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 34
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 14
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(z, cons(s(s(z)), cons(s(s(z)), cons(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 20, which took 0.085385 s (model generation: 0.064348,  model checking: 0.021037):

Model:
|_
{
append -> 
{{{
Q={q_gen_463, q_gen_468, q_gen_469, q_gen_480, q_gen_481, q_gen_482},
Q_f={q_gen_463},
Delta=
{
<cons>(q_gen_481, q_gen_480) -> q_gen_480
<nil>() -> q_gen_480
<s>(q_gen_481) -> q_gen_481
<z>() -> q_gen_481
<cons, cons>(q_gen_469, q_gen_468) -> q_gen_468
<nil, cons>(q_gen_481, q_gen_480) -> q_gen_468
<nil, nil>() -> q_gen_468
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_481) -> q_gen_469
<z, s>(q_gen_481) -> q_gen_469
<z, z>() -> q_gen_469
<cons, cons, cons>(q_gen_482, q_gen_463) -> q_gen_463
<cons, nil, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, cons, cons>(q_gen_469, q_gen_468) -> q_gen_463
<nil, nil, cons>(q_gen_481, q_gen_480) -> q_gen_463
<nil, nil, nil>() -> q_gen_463
<s, s, s>(q_gen_482) -> q_gen_482
<s, s, z>(q_gen_469) -> q_gen_482
<s, z, s>(q_gen_469) -> q_gen_482
<s, z, z>(q_gen_481) -> q_gen_482
<z, s, z>(q_gen_481) -> q_gen_482
<z, z, s>(q_gen_481) -> q_gen_482
<z, z, z>() -> q_gen_482
}

Datatype: <natlist, natlist, natlist>
Convolution form: right
}}}
  ;  length -> 
{{{
Q={q_gen_462, q_gen_466},
Q_f={q_gen_462},
Delta=
{
<s>(q_gen_466) -> q_gen_466
<z>() -> q_gen_466
<cons, s>(q_gen_466, q_gen_462) -> q_gen_462
<nil, z>() -> q_gen_462
}

Datatype: <natlist, nat>
Convolution form: right
}}}
  ;  leq -> 
{{{
Q={q_gen_459, q_gen_461},
Q_f={q_gen_459},
Delta=
{
<s>(q_gen_461) -> q_gen_461
<z>() -> q_gen_461
<s, s>(q_gen_459) -> q_gen_459
<z, s>(q_gen_461) -> q_gen_459
<z, z>() -> q_gen_459
}

Datatype: <nat, nat>
Convolution form: right
}}}

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> length([nil, z]) -> 14
() -> leq([z, s(nn2)]) -> 16
() -> leq([z, z]) -> 14
(append([l1, l2, _cc]) /\ length([_cc, _dc]) /\ length([l1, _bc])) -> leq([_bc, _dc]) -> 14
(append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]) -> 37
(length([ll, _xb])) -> length([cons(x, ll), s(_xb)]) -> 17
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15
(leq([s(nn1), z])) -> BOT -> 15
}
Sat witness: Found: ((append([t1, l2, _sb])) -> append([cons(h1, t1), l2, cons(h1, _sb)]), {
_sb -> cons(s(s(z)), cons(s(s(z)), cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(z, cons(s(s(z)), nil)))  ;  t1 -> cons(s(z), cons(s(z), nil))
})

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