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


Learning problem is:

env: {
nat -> {s, z}  ;  natlist -> {cons, nil}
}
definition:
{
(append, F:
{() -> append([nil, l2, l2])
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)])}
(append([_fb, _gb, _hb]) /\ append([_fb, _gb, _ib])) -> eq_natlist([_hb, _ib])
)
(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, _jb])) -> length([cons(x, ll), s(_jb)])}
(length([_kb, _lb]) /\ length([_kb, _mb])) -> eq_nat([_lb, _mb])
)
}

properties:
{(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb])}


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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 0
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 0
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.000676 seconds.
DontKnow. Stopped because: timeout
Working model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_442, q_gen_443, q_gen_444, q_gen_447, q_gen_448, q_gen_449, q_gen_453, q_gen_454, q_gen_455, q_gen_456, q_gen_457, q_gen_458, q_gen_462, q_gen_463, q_gen_467, q_gen_471, q_gen_475, q_gen_476, q_gen_477, q_gen_478, q_gen_479, q_gen_491, q_gen_492, q_gen_493, q_gen_494, q_gen_497, q_gen_498, q_gen_499, q_gen_500, q_gen_501, q_gen_502, q_gen_507, q_gen_510, q_gen_511, q_gen_512, q_gen_513, q_gen_514, q_gen_515, q_gen_521, q_gen_522, q_gen_523, q_gen_524, 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_540, q_gen_541, q_gen_542, q_gen_543, q_gen_544, q_gen_545, q_gen_546, q_gen_547, q_gen_548, q_gen_549, q_gen_552, q_gen_553, q_gen_554, q_gen_555, q_gen_556, q_gen_557, q_gen_558, q_gen_559, q_gen_560, q_gen_561, q_gen_562, q_gen_563, q_gen_564, q_gen_565, q_gen_566, q_gen_569, q_gen_570, q_gen_571, q_gen_572, q_gen_573, q_gen_574, q_gen_575, q_gen_576, q_gen_577, q_gen_578, q_gen_585, q_gen_586, q_gen_587, q_gen_588, q_gen_589, q_gen_590, q_gen_591, q_gen_592, q_gen_593, q_gen_594, q_gen_595, q_gen_596, q_gen_597},
Q_f={},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons>(q_gen_457, q_gen_456) -> q_gen_478
<s>(q_gen_457) -> q_gen_500
<s>(q_gen_556) -> q_gen_555
<s>(q_gen_500) -> q_gen_556
<nil, nil>() -> q_gen_443
<z, z>() -> q_gen_444
<cons, cons>(q_gen_449, q_gen_443) -> q_gen_448
<s, s>(q_gen_444) -> q_gen_449
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_463
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_494
<cons, cons>(q_gen_444, q_gen_514) -> q_gen_513
<cons, cons>(q_gen_444, q_gen_515) -> q_gen_514
<nil, cons>(q_gen_457, q_gen_478) -> q_gen_515
<cons, cons>(q_gen_449, q_gen_463) -> q_gen_528
<nil, cons>(q_gen_500, q_gen_478) -> q_gen_531
<s, z>(q_gen_457) -> q_gen_532
<cons, cons>(q_gen_444, q_gen_549) -> q_gen_548
<cons, cons>(q_gen_444, q_gen_463) -> q_gen_549
<s, s>(q_gen_532) -> q_gen_558
<z, s>(q_gen_457) -> q_gen_564
<cons, cons>(q_gen_444, q_gen_494) -> q_gen_566
<s, z>(q_gen_500) -> q_gen_588
<cons, cons>(q_gen_444, q_gen_597) -> q_gen_596
<nil, cons>(q_gen_500, q_gen_456) -> q_gen_597
<nil, nil, nil>() -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_442
<nil, cons, cons>(q_gen_449, q_gen_448) -> q_gen_447
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_453
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_454
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<z, z, z>() -> q_gen_458
<cons, nil, cons>(q_gen_444, q_gen_463) -> q_gen_462
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_467
<cons, cons, cons>(q_gen_458, q_gen_462) -> q_gen_471
<nil, cons, cons>(q_gen_444, q_gen_463) -> q_gen_475
<cons, cons, cons>(q_gen_458, q_gen_477) -> q_gen_476
<nil, nil, cons>(q_gen_457, q_gen_478) -> q_gen_477
<cons, nil, cons>(q_gen_449, q_gen_463) -> q_gen_479
<cons, cons, cons>(q_gen_492, q_gen_477) -> q_gen_491
<s, z, s>(q_gen_444) -> q_gen_492
<cons, nil, cons>(q_gen_444, q_gen_494) -> q_gen_493
<nil, cons, cons>(q_gen_449, q_gen_463) -> q_gen_497
<cons, cons, cons>(q_gen_501, q_gen_499) -> q_gen_498
<nil, nil, cons>(q_gen_500, q_gen_478) -> q_gen_499
<s, s, s>(q_gen_458) -> q_gen_501
<cons, cons, cons>(q_gen_458, q_gen_453) -> q_gen_502
<cons, cons, cons>(q_gen_458, q_gen_467) -> q_gen_507
<nil, cons, cons>(q_gen_444, q_gen_494) -> q_gen_510
<cons, cons, cons>(q_gen_492, q_gen_475) -> q_gen_511
<cons, nil, cons>(q_gen_444, q_gen_513) -> q_gen_512
<cons, cons, cons>(q_gen_501, q_gen_455) -> q_gen_521
<cons, cons, cons>(q_gen_523, q_gen_479) -> q_gen_522
<z, s, z>(q_gen_457) -> q_gen_523
<cons, cons, cons>(q_gen_492, q_gen_453) -> q_gen_524
<nil, cons, cons>(q_gen_444, q_gen_528) -> q_gen_527
<cons, cons, cons>(q_gen_492, q_gen_530) -> q_gen_529
<nil, cons, cons>(q_gen_532, q_gen_531) -> q_gen_530
<cons, cons, cons>(q_gen_458, q_gen_534) -> q_gen_533
<cons, cons, cons>(q_gen_501, q_gen_453) -> q_gen_534
<cons, cons, cons>(q_gen_542, q_gen_541) -> q_gen_540
<nil, cons, cons>(q_gen_532, q_gen_494) -> q_gen_541
<s, z, s>(q_gen_532) -> q_gen_542
<cons, cons, cons>(q_gen_492, q_gen_544) -> q_gen_543
<cons, cons, cons>(q_gen_545, q_gen_475) -> q_gen_544
<s, s, s>(q_gen_546) -> q_gen_545
<s, z, z>(q_gen_457) -> q_gen_546
<cons, nil, cons>(q_gen_444, q_gen_548) -> q_gen_547
<cons, cons, cons>(q_gen_557, q_gen_553) -> q_gen_552
<cons, cons, cons>(q_gen_554, q_gen_455) -> q_gen_553
<z, s, z>(q_gen_555) -> q_gen_554
<s, z, s>(q_gen_558) -> q_gen_557
<cons, cons, cons>(q_gen_458, q_gen_560) -> q_gen_559
<cons, cons, cons>(q_gen_561, q_gen_462) -> q_gen_560
<s, s, s>(q_gen_562) -> q_gen_561
<s, s, s>(q_gen_563) -> q_gen_562
<s, s, z>(q_gen_564) -> q_gen_563
<cons, nil, cons>(q_gen_449, q_gen_566) -> q_gen_565
<cons, cons, cons>(q_gen_492, q_gen_570) -> q_gen_569
<cons, cons, cons>(q_gen_572, q_gen_571) -> q_gen_570
<nil, cons, cons>(q_gen_532, q_gen_443) -> q_gen_571
<s, z, s>(q_gen_564) -> q_gen_572
<cons, cons, cons>(q_gen_492, q_gen_574) -> q_gen_573
<cons, cons, cons>(q_gen_492, q_gen_575) -> q_gen_574
<cons, cons, cons>(q_gen_576, q_gen_455) -> q_gen_575
<s, s, s>(q_gen_577) -> q_gen_576
<z, z, s>(q_gen_457) -> q_gen_577
<cons, cons, cons>(q_gen_523, q_gen_477) -> q_gen_578
<cons, cons, cons>(q_gen_589, q_gen_586) -> q_gen_585
<cons, cons, cons>(q_gen_572, q_gen_587) -> q_gen_586
<nil, cons, cons>(q_gen_588, q_gen_443) -> q_gen_587
<s, z, s>(q_gen_449) -> q_gen_589
<cons, cons, cons>(q_gen_492, q_gen_591) -> q_gen_590
<cons, cons, cons>(q_gen_589, q_gen_592) -> q_gen_591
<cons, cons, cons>(q_gen_593, q_gen_455) -> q_gen_592
<s, s, s>(q_gen_594) -> q_gen_593
<z, s, s>(q_gen_444) -> q_gen_594
<cons, nil, cons>(q_gen_444, q_gen_596) -> q_gen_595
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_439, q_gen_440, q_gen_441, q_gen_450, q_gen_451, q_gen_452, q_gen_459, q_gen_460, q_gen_461, q_gen_464, q_gen_465, q_gen_466, q_gen_468, q_gen_472, q_gen_473, q_gen_474, q_gen_480, q_gen_481, q_gen_482, q_gen_483, q_gen_486, q_gen_487, q_gen_488, q_gen_489, q_gen_490, q_gen_495, q_gen_496, q_gen_503, q_gen_504, q_gen_505, q_gen_506, q_gen_508, q_gen_509, q_gen_516, q_gen_517, q_gen_518, q_gen_519, q_gen_520, q_gen_525, q_gen_526, q_gen_535, q_gen_536, q_gen_537, q_gen_538, q_gen_539, q_gen_550, q_gen_551, q_gen_567, q_gen_568, q_gen_579, q_gen_582, q_gen_583, q_gen_584, q_gen_598, q_gen_599, q_gen_600, q_gen_601},
Q_f={},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_487
<cons>(q_gen_452, q_gen_473) -> q_gen_506
<cons>(q_gen_452, q_gen_506) -> q_gen_517
<cons>(q_gen_461, q_gen_487) -> q_gen_520
<cons>(q_gen_461, q_gen_440) -> q_gen_537
<s>(q_gen_461) -> q_gen_584
<cons>(q_gen_452, q_gen_537) -> q_gen_599
<nil, z>() -> q_gen_436
<cons, s>(q_gen_441, q_gen_440) -> q_gen_439
<z, z>() -> q_gen_441
<cons, s>(q_gen_451, q_gen_440) -> q_gen_450
<s, z>(q_gen_452) -> q_gen_451
<cons, s>(q_gen_460, q_gen_440) -> q_gen_459
<s, z>(q_gen_461) -> q_gen_460
<cons, s>(q_gen_466, q_gen_465) -> q_gen_464
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_473) -> q_gen_472
<s, s>(q_gen_466) -> q_gen_474
<cons, s>(q_gen_474, q_gen_465) -> q_gen_480
<cons, s>(q_gen_482, q_gen_440) -> q_gen_481
<s, s>(q_gen_483) -> q_gen_482
<z, s>(q_gen_461) -> q_gen_483
<cons, s>(q_gen_488, q_gen_487) -> q_gen_486
<s, s>(q_gen_489) -> q_gen_488
<s, s>(q_gen_490) -> q_gen_489
<s, s>(q_gen_441) -> q_gen_490
<cons, s>(q_gen_483, q_gen_465) -> q_gen_495
<cons, s>(q_gen_490, q_gen_465) -> q_gen_496
<cons, s>(q_gen_483, q_gen_440) -> q_gen_503
<cons, s>(q_gen_466, q_gen_473) -> q_gen_504
<cons, s>(q_gen_483, q_gen_506) -> q_gen_505
<cons, s>(q_gen_441, q_gen_465) -> q_gen_508
<cons, s>(q_gen_483, q_gen_473) -> q_gen_509
<cons, s>(q_gen_466, q_gen_517) -> q_gen_516
<cons, s>(q_gen_490, q_gen_487) -> q_gen_518
<cons, s>(q_gen_474, q_gen_520) -> q_gen_519
<cons, s>(q_gen_474, q_gen_440) -> q_gen_525
<cons, s>(q_gen_483, q_gen_487) -> q_gen_526
<cons, s>(q_gen_441, q_gen_487) -> q_gen_535
<cons, s>(q_gen_466, q_gen_537) -> q_gen_536
<cons, s>(q_gen_539, q_gen_537) -> q_gen_538
<s, s>(q_gen_482) -> q_gen_539
<cons, s>(q_gen_466, q_gen_506) -> q_gen_550
<cons, s>(q_gen_490, q_gen_537) -> q_gen_551
<cons, s>(q_gen_482, q_gen_473) -> q_gen_567
<cons, s>(q_gen_482, q_gen_506) -> q_gen_568
<cons, s>(q_gen_441, q_gen_473) -> q_gen_579
<cons, s>(q_gen_583, q_gen_440) -> q_gen_582
<s, z>(q_gen_584) -> q_gen_583
<cons, s>(q_gen_483, q_gen_599) -> q_gen_598
<cons, s>(q_gen_601, q_gen_465) -> q_gen_600
<z, s>(q_gen_584) -> q_gen_601
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_434, q_gen_435, q_gen_438, q_gen_445, q_gen_446, q_gen_469, q_gen_470, q_gen_484, q_gen_485, q_gen_580, q_gen_581},
Q_f={},
Delta=
{
<z>() -> q_gen_435
<s>(q_gen_435) -> q_gen_446
<z, z>() -> q_gen_433
<z, s>(q_gen_435) -> q_gen_434
<s, s>(q_gen_433) -> q_gen_438
<z, s>(q_gen_446) -> q_gen_445
<s, s>(q_gen_470) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_470
<s, s>(q_gen_485) -> q_gen_484
<s, s>(q_gen_469) -> q_gen_485
<s, s>(q_gen_581) -> q_gen_580
<s, z>(q_gen_446) -> q_gen_581
}

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

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

-------------------
STEPS:
-------------------------------------------
Step 0, which took 0.039921 s (model generation: 0.039500,  model checking: 0.000421):

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

}

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

}

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

}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 1
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.010610 s (model generation: 0.010521,  model checking: 0.000089):

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

}

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

}

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

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 1
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.009058 s (model generation: 0.008990,  model checking: 0.000068):

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

}

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

}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<z>() -> q_gen_435
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 1
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.007972 s (model generation: 0.007826,  model checking: 0.000146):

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

}

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

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<z>() -> q_gen_435
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 1
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.007561 s (model generation: 0.007449,  model checking: 0.000112):

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

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

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<z>() -> q_gen_435
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 1
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.008089 s (model generation: 0.007596,  model checking: 0.000493):

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

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

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 1
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> z  ;  ll -> nil  ;  x -> z
})

-------------------------------------------
Step 6, which took 0.008278 s (model generation: 0.008097,  model checking: 0.000181):

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

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 1
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 4
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> nil  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 7, which took 0.009229 s (model generation: 0.008919,  model checking: 0.000310):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444},
Q_f={q_gen_437},
Delta=
{
<nil, nil>() -> q_gen_443
<z, z>() -> q_gen_444
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 2
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 4
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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.009196 s (model generation: 0.008485,  model checking: 0.000711):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444},
Q_f={q_gen_437},
Delta=
{
<nil, nil>() -> q_gen_443
<z, z>() -> q_gen_444
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 3
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 4
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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(s(z), nil))
})

-------------------------------------------
Step 9, which took 0.009054 s (model generation: 0.008625,  model checking: 0.000429):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444},
Q_f={q_gen_437},
Delta=
{
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 4
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 4
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> z  ;  ll -> nil  ;  x -> s(z)
})

-------------------------------------------
Step 10, which took 0.010410 s (model generation: 0.009130,  model checking: 0.001280):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444},
Q_f={q_gen_437},
Delta=
{
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 4
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 7
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 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, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 11, which took 0.011234 s (model generation: 0.010232,  model checking: 0.001002):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

}
--
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, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 5
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 7
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 10
(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: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> z  ;  ll -> nil  ;  x -> s(s(z))
})

-------------------------------------------
Step 12, which took 0.012431 s (model generation: 0.011492,  model checking: 0.000939):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 7
() -> length([nil, z]) -> 6
() -> leq([z, s(nn2)]) -> 7
() -> leq([z, z]) -> 6
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 6
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 10
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 10
(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, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> nil
})

-------------------------------------------
Step 13, which took 0.012790 s (model generation: 0.011671,  model checking: 0.001119):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 7
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 7
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 10
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 13
(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: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(z)  ;  ll -> cons(z, nil)  ;  x -> z
})

-------------------------------------------
Step 14, which took 0.019219 s (model generation: 0.018689,  model checking: 0.000530):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, s>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 7
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 7
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 10
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 10
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 13
(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([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(z))  ;  _ob -> cons(z, nil)  ;  _pb -> s(z)  ;  l1 -> cons(z, nil)  ;  l2 -> cons(z, nil)
})

-------------------------------------------
Step 15, which took 0.014750 s (model generation: 0.014584,  model checking: 0.000166):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, s>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<s, z>(q_gen_435) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 8
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 8
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 10
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 10
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 8
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((leq([s(nn1), z])) -> BOT, {
nn1 -> z
})

-------------------------------------------
Step 16, which took 0.014382 s (model generation: 0.013886,  model checking: 0.000496):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, s>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_470},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<s, s>(q_gen_470) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, z>(q_gen_435) -> q_gen_470
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 8
() -> length([nil, z]) -> 8
() -> leq([z, s(nn2)]) -> 8
() -> leq([z, z]) -> 8
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 10
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 10
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 8
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(z)  ;  nn2 -> z
})

-------------------------------------------
Step 17, which took 0.016685 s (model generation: 0.015611,  model checking: 0.001074):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_455, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_455
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, s>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 9
() -> length([nil, z]) -> 9
() -> leq([z, s(nn2)]) -> 9
() -> leq([z, z]) -> 9
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 10
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 13
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 9
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 18, which took 0.015600 s (model generation: 0.014646,  model checking: 0.000954):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_442, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458, q_gen_467},
Q_f={q_gen_437, q_gen_442},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_442) -> q_gen_442
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_442
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_442
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_442
<z, z, z>() -> q_gen_458
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_467
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, s>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 10
() -> length([nil, z]) -> 10
() -> leq([z, s(nn2)]) -> 10
() -> leq([z, z]) -> 10
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 13
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 13
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 13
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 10
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 11
(leq([s(nn1), z])) -> BOT -> 11
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(z))  ;  _ob -> cons(z, nil)  ;  _pb -> s(z)  ;  l1 -> cons(z, nil)  ;  l2 -> nil
})

-------------------------------------------
Step 19, which took 0.016188 s (model generation: 0.014575,  model checking: 0.001613):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 11
() -> length([nil, z]) -> 11
() -> leq([z, s(nn2)]) -> 11
() -> leq([z, z]) -> 11
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 13
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 13
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 11
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 12
(leq([s(nn1), z])) -> BOT -> 12
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(z))  ;  ll -> cons(z, cons(z, nil))  ;  x -> s(z)
})

-------------------------------------------
Step 20, which took 0.017266 s (model generation: 0.015457,  model checking: 0.001809):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 12
() -> length([nil, z]) -> 12
() -> leq([z, s(nn2)]) -> 12
() -> leq([z, z]) -> 12
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 13
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 16
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 12
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 13
(leq([s(nn1), z])) -> BOT -> 13
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 21, which took 0.019340 s (model generation: 0.017230,  model checking: 0.002110):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 13
() -> length([nil, z]) -> 13
() -> leq([z, s(nn2)]) -> 13
() -> leq([z, z]) -> 13
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 16
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 16
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 16
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 13
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 14
(leq([s(nn1), z])) -> BOT -> 14
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(s(z))))  ;  _ob -> cons(s(z), cons(z, nil))  ;  _pb -> s(s(s(z)))  ;  l1 -> cons(s(z), nil)  ;  l2 -> nil
})

-------------------------------------------
Step 22, which took 0.022863 s (model generation: 0.020915,  model checking: 0.001948):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 14
() -> length([nil, z]) -> 14
() -> leq([z, s(nn2)]) -> 14
() -> leq([z, z]) -> 14
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 16
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 16
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 14
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 15
(leq([s(nn1), z])) -> BOT -> 15
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(s(z)))  ;  ll -> cons(s(z), cons(z, nil))  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 23, which took 0.027022 s (model generation: 0.024001,  model checking: 0.003021):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_441) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 15
() -> length([nil, z]) -> 15
() -> leq([z, s(nn2)]) -> 15
() -> leq([z, z]) -> 15
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 16
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 19
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 15
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 16
(leq([s(nn1), z])) -> BOT -> 16
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, nil)  ;  t1 -> nil
})

-------------------------------------------
Step 24, which took 0.026805 s (model generation: 0.024697,  model checking: 0.002108):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 16
() -> length([nil, z]) -> 16
() -> leq([z, s(nn2)]) -> 16
() -> leq([z, z]) -> 16
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 19
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 19
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 19
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 16
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 17
(leq([s(nn1), z])) -> BOT -> 17
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(z)))  ;  _ob -> cons(z, cons(z, nil))  ;  _pb -> s(s(z))  ;  l1 -> cons(z, cons(z, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 25, which took 0.030009 s (model generation: 0.028081,  model checking: 0.001928):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_441) -> q_gen_441
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 17
() -> length([nil, z]) -> 17
() -> leq([z, s(nn2)]) -> 17
() -> leq([z, z]) -> 17
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 19
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 19
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 17
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 18
(leq([s(nn1), z])) -> BOT -> 18
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(z)  ;  ll -> cons(z, nil)  ;  x -> s(z)
})

-------------------------------------------
Step 26, which took 0.034704 s (model generation: 0.030231,  model checking: 0.004473):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 18
() -> length([nil, z]) -> 18
() -> leq([z, s(nn2)]) -> 18
() -> leq([z, z]) -> 18
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 19
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 22
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 18
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 19
(leq([s(nn1), z])) -> BOT -> 19
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(s(z), cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(s(z), nil)  ;  t1 -> nil
})

-------------------------------------------
Step 27, which took 0.033950 s (model generation: 0.033174,  model checking: 0.000776):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_441) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469, q_gen_470},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<s, s>(q_gen_469) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_470) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_470
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> length([nil, z]) -> 19
() -> leq([z, s(nn2)]) -> 19
() -> leq([z, z]) -> 19
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 19
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 22
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 19
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: ((leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]), {
nn1 -> s(s(z))  ;  nn2 -> s(z)
})

-------------------------------------------
Step 28, which took 0.042156 s (model generation: 0.039494,  model checking: 0.002662):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons>(q_gen_461, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 19
() -> length([nil, z]) -> 19
() -> leq([z, s(nn2)]) -> 19
() -> leq([z, z]) -> 19
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 22
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 22
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(z)))  ;  _ob -> cons(z, cons(z, nil))  ;  _pb -> s(s(z))  ;  l1 -> cons(z, nil)  ;  l2 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 29, which took 0.038666 s (model generation: 0.038015,  model checking: 0.000651):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_448, q_gen_453, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_448
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_448) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_453
<cons, cons, cons>(q_gen_458, q_gen_453) -> q_gen_453
<cons, nil, cons>(q_gen_444, q_gen_448) -> q_gen_453
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_453
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_453
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_441) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 20
() -> leq([z, s(nn2)]) -> 20
() -> leq([z, z]) -> 20
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 22
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 22
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 22
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 20
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 22
(leq([s(nn1), z])) -> BOT -> 20
}
Sat witness: Found: (() -> append([nil, l2, l2]), {
l2 -> cons(z, nil)
})

-------------------------------------------
Step 30, which took 0.041344 s (model generation: 0.038601,  model checking: 0.002743):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_483},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons>(q_gen_461, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_483) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_465) -> q_gen_468
<z, s>(q_gen_461) -> q_gen_483
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 21
() -> leq([z, s(nn2)]) -> 21
() -> leq([z, z]) -> 21
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 22
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 22
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 21
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 21
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(z))  ;  ll -> cons(z, cons(z, cons(z, nil)))  ;  x -> z
})

-------------------------------------------
Step 31, which took 0.041783 s (model generation: 0.040976,  model checking: 0.000807):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_448, q_gen_456, q_gen_457, q_gen_458, q_gen_493},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_448
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_448) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
<cons, nil, cons>(q_gen_444, q_gen_448) -> q_gen_493
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<s>(q_gen_452) -> q_gen_452
<z>() -> q_gen_452
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_441) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_466) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 22
() -> leq([z, s(nn2)]) -> 22
() -> leq([z, z]) -> 22
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 22
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 25
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 22
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 22
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, nil)  ;  h1 -> z  ;  l2 -> nil  ;  t1 -> cons(z, nil)
})

-------------------------------------------
Step 32, which took 0.043141 s (model generation: 0.041199,  model checking: 0.001942):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_482},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_465) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_441) -> q_gen_441
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_482, q_gen_440) -> q_gen_468
<cons, s>(q_gen_482, q_gen_465) -> q_gen_468
<s, s>(q_gen_482) -> q_gen_482
<z, s>(q_gen_461) -> q_gen_482
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 22
() -> length([nil, z]) -> 22
() -> leq([z, s(nn2)]) -> 22
() -> leq([z, z]) -> 22
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 25
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 25
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 25
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 23
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 23
(leq([s(nn1), z])) -> BOT -> 23
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(z))  ;  _ob -> cons(z, cons(z, nil))  ;  _pb -> s(z)  ;  l1 -> cons(z, cons(z, nil))  ;  l2 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 33, which took 0.046052 s (model generation: 0.041864,  model checking: 0.004188):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_483},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_483) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_465) -> q_gen_468
<z, s>(q_gen_461) -> q_gen_483
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 23
() -> length([nil, z]) -> 23
() -> leq([z, s(nn2)]) -> 23
() -> leq([z, z]) -> 23
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 25
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 25
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 24
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 24
(leq([s(nn1), z])) -> BOT -> 24
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(z))  ;  ll -> cons(z, cons(z, nil))  ;  x -> z
})

-------------------------------------------
Step 34, which took 0.048709 s (model generation: 0.047374,  model checking: 0.001335):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_447, q_gen_455, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437, q_gen_447},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_447
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_447
<cons, cons, cons>(q_gen_458, q_gen_447) -> q_gen_455
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 24
() -> length([nil, z]) -> 24
() -> leq([z, s(nn2)]) -> 24
() -> leq([z, z]) -> 24
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 25
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 28
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 25
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 25
(leq([s(nn1), z])) -> BOT -> 25
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, cons(z, nil))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(z, nil))  ;  t1 -> nil
})

-------------------------------------------
Step 35, which took 0.062628 s (model generation: 0.058522,  model checking: 0.004106):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_483},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_473) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_473) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_483, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_483) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_483, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_465) -> q_gen_468
<z, s>(q_gen_461) -> q_gen_483
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 25
() -> length([nil, z]) -> 25
() -> leq([z, s(nn2)]) -> 25
() -> leq([z, z]) -> 25
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 28
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 28
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 28
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 26
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 26
(leq([s(nn1), z])) -> BOT -> 26
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(z)))  ;  _ob -> cons(z, cons(z, cons(z, cons(z, cons(z, nil)))))  ;  _pb -> s(s(z))  ;  l1 -> cons(z, cons(z, cons(z, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 36, which took 0.066850 s (model generation: 0.061822,  model checking: 0.005028):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_473) -> q_gen_465
<cons>(q_gen_461, q_gen_465) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_474) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 26
() -> length([nil, z]) -> 26
() -> leq([z, s(nn2)]) -> 26
() -> leq([z, z]) -> 26
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 28
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 28
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 27
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 27
(leq([s(nn1), z])) -> BOT -> 27
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(z))  ;  ll -> cons(s(z), cons(s(z), cons(z, nil)))  ;  x -> s(z)
})

-------------------------------------------
Step 37, which took 0.069338 s (model generation: 0.064517,  model checking: 0.004821):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_483},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_473) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_440) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_473) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_483, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_483) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_483, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_465) -> q_gen_468
<z, s>(q_gen_461) -> q_gen_483
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 27
() -> length([nil, z]) -> 27
() -> leq([z, s(nn2)]) -> 27
() -> leq([z, z]) -> 27
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 28
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 31
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 28
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 28
(leq([s(nn1), z])) -> BOT -> 28
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(s(z), cons(z, nil))  ;  h1 -> z  ;  l2 -> cons(s(z), nil)  ;  t1 -> cons(s(z), nil)
})

-------------------------------------------
Step 38, which took 0.075643 s (model generation: 0.069947,  model checking: 0.005696):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_483},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_440) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_473) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_483, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_483) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_483, q_gen_440) -> q_gen_468
<cons, s>(q_gen_483, q_gen_465) -> q_gen_468
<z, s>(q_gen_461) -> q_gen_483
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 28
() -> length([nil, z]) -> 28
() -> leq([z, s(nn2)]) -> 28
() -> leq([z, z]) -> 28
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 31
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 31
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 31
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 29
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 29
(leq([s(nn1), z])) -> BOT -> 29
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(z)))  ;  _ob -> cons(s(z), cons(z, nil))  ;  _pb -> s(s(z))  ;  l1 -> cons(s(z), nil)  ;  l2 -> cons(z, cons(z, nil))
})

-------------------------------------------
Step 39, which took 0.083604 s (model generation: 0.081277,  model checking: 0.002327):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_440) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_474) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 29
() -> length([nil, z]) -> 29
() -> leq([z, s(nn2)]) -> 29
() -> leq([z, z]) -> 29
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 31
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 31
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 30
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 30
(leq([s(nn1), z])) -> BOT -> 30
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(z))  ;  ll -> cons(s(z), cons(z, nil))  ;  x -> z
})

-------------------------------------------
Step 40, which took 0.087982 s (model generation: 0.078603,  model checking: 0.009379):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_461, q_gen_473) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<s, s>(q_gen_474) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 30
() -> length([nil, z]) -> 30
() -> leq([z, s(nn2)]) -> 30
() -> leq([z, z]) -> 30
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 31
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 34
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 31
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 31
(leq([s(nn1), z])) -> BOT -> 31
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(z, cons(s(z), cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), nil))  ;  t1 -> nil
})

-------------------------------------------
Step 41, which took 0.088828 s (model generation: 0.085492,  model checking: 0.003336):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_455, q_gen_456, q_gen_457, q_gen_458, q_gen_463},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<cons, cons>(q_gen_444, q_gen_463) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_463
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_455
<cons, nil, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, cons, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 31
() -> length([nil, z]) -> 31
() -> leq([z, s(nn2)]) -> 31
() -> leq([z, z]) -> 31
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 34
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 34
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 34
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 32
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 32
(leq([s(nn1), z])) -> BOT -> 32
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(z))  ;  _ob -> cons(z, cons(s(z), cons(z, nil)))  ;  _pb -> s(z)  ;  l1 -> cons(z, cons(s(z), nil))  ;  l2 -> cons(z, cons(s(z), cons(z, nil)))
})

-------------------------------------------
Step 42, which took 0.117151 s (model generation: 0.106145,  model checking: 0.011006):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_461, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_473) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_473) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_473) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 32
() -> length([nil, z]) -> 32
() -> leq([z, s(nn2)]) -> 32
() -> leq([z, z]) -> 32
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 34
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 34
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 37
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 33
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 33
(leq([s(nn1), z])) -> BOT -> 33
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(s(s(z))))  ;  ll -> cons(s(z), nil)  ;  x -> s(s(z))
})

-------------------------------------------
Step 43, which took 0.131781 s (model generation: 0.111127,  model checking: 0.020654):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_473) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_473) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 33
() -> length([nil, z]) -> 33
() -> leq([z, s(nn2)]) -> 33
() -> leq([z, z]) -> 33
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 34
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 37
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 37
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 34
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 34
(leq([s(nn1), z])) -> BOT -> 34
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(s(z), cons(z, cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(s(z), cons(z, nil)))  ;  t1 -> cons(s(s(z)), nil)
})

-------------------------------------------
Step 44, which took 0.163141 s (model generation: 0.157696,  model checking: 0.005445):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_461, q_gen_440) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_473) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_473) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<s, s>(q_gen_474) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 34
() -> length([nil, z]) -> 34
() -> leq([z, s(nn2)]) -> 34
() -> leq([z, z]) -> 34
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 37
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 37
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 37
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 35
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 35
(leq([s(nn1), z])) -> BOT -> 35
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(z)))  ;  _ob -> cons(z, cons(z, cons(z, cons(z, nil))))  ;  _pb -> s(s(z))  ;  l1 -> cons(z, cons(z, cons(z, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 45, which took 0.162230 s (model generation: 0.160252,  model checking: 0.001978):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_440) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_473) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<s, s>(q_gen_474) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 35
() -> length([nil, z]) -> 35
() -> leq([z, s(nn2)]) -> 35
() -> leq([z, z]) -> 35
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 37
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 37
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 40
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 36
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 36
(leq([s(nn1), z])) -> BOT -> 36
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(z)  ;  ll -> cons(s(z), nil)  ;  x -> s(z)
})

-------------------------------------------
Step 46, which took 0.179782 s (model generation: 0.162083,  model checking: 0.017699):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_473) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 36
() -> length([nil, z]) -> 36
() -> leq([z, s(nn2)]) -> 36
() -> leq([z, z]) -> 36
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 37
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 40
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 40
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 37
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 37
(leq([s(nn1), z])) -> BOT -> 37
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(s(s(z)), cons(z, cons(z, nil)))  ;  h1 -> z  ;  l2 -> cons(z, cons(s(s(s(s(z)))), nil))  ;  t1 -> cons(s(s(s(z))), cons(z, nil))
})

-------------------------------------------
Step 47, which took 0.246515 s (model generation: 0.240775,  model checking: 0.005740):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, s, z>(q_gen_444) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_473) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<s, s>(q_gen_474) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 37
() -> length([nil, z]) -> 37
() -> leq([z, s(nn2)]) -> 37
() -> leq([z, z]) -> 37
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 40
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 40
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 40
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 38
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 38
(leq([s(nn1), z])) -> BOT -> 38
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(s(z))))  ;  _ob -> cons(s(z), cons(z, cons(z, nil)))  ;  _pb -> s(s(s(z)))  ;  l1 -> cons(s(z), cons(z, cons(z, nil)))  ;  l2 -> nil
})

-------------------------------------------
Step 48, which took 0.272641 s (model generation: 0.267089,  model checking: 0.005552):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, s, z>(q_gen_444) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_473) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_473) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 38
() -> length([nil, z]) -> 38
() -> leq([z, s(nn2)]) -> 38
() -> leq([z, z]) -> 38
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 40
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 40
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 43
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 39
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 39
(leq([s(nn1), z])) -> BOT -> 39
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(s(z)))  ;  ll -> cons(z, cons(z, cons(z, nil)))  ;  x -> s(z)
})

-------------------------------------------
Step 49, which took 0.390613 s (model generation: 0.352119,  model checking: 0.038494):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, s, z>(q_gen_444) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474, q_gen_506},
Q_f={q_gen_436},
Delta=
{
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_506
<cons>(q_gen_452, q_gen_506) -> q_gen_506
<cons>(q_gen_461, q_gen_473) -> q_gen_506
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_506) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_473) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<cons, s>(q_gen_474, q_gen_506) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_506) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 39
() -> length([nil, z]) -> 39
() -> leq([z, s(nn2)]) -> 39
() -> leq([z, z]) -> 39
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 40
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 43
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 43
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 40
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 40
(leq([s(nn1), z])) -> BOT -> 40
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(s(z), cons(s(s(z)), cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(z, cons(s(z), nil)))  ;  t1 -> cons(s(z), cons(s(z), nil))
})

-------------------------------------------
Step 50, which took 0.581061 s (model generation: 0.577398,  model checking: 0.003663):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_455, q_gen_456, q_gen_457, q_gen_458, q_gen_463, q_gen_467},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons>(q_gen_444, q_gen_463) -> q_gen_463
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_463
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_467) -> q_gen_455
<cons, nil, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, cons, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<s, s, s>(q_gen_458) -> q_gen_458
<s, s, z>(q_gen_444) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, s>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_467
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 40
() -> length([nil, z]) -> 40
() -> leq([z, s(nn2)]) -> 40
() -> leq([z, z]) -> 40
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 43
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 43
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 43
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 41
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 41
(leq([s(nn1), z])) -> BOT -> 41
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(z)))  ;  _ob -> cons(z, cons(z, cons(z, nil)))  ;  _pb -> s(z)  ;  l1 -> cons(z, nil)  ;  l2 -> cons(s(z), nil)
})

-------------------------------------------
Step 51, which took 0.565984 s (model generation: 0.559890,  model checking: 0.006094):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_455, q_gen_456, q_gen_457, q_gen_458, q_gen_463, q_gen_501},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons>(q_gen_444, q_gen_463) -> q_gen_463
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_463
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_437
<cons, cons, cons>(q_gen_501, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_455
<cons, cons, cons>(q_gen_501, q_gen_455) -> q_gen_455
<cons, nil, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, cons, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<s, s, s>(q_gen_501) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
<s, s, s>(q_gen_458) -> q_gen_501
<s, s, z>(q_gen_444) -> q_gen_501
<z, s, z>(q_gen_457) -> q_gen_501
<z, z, s>(q_gen_457) -> q_gen_501
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 41
() -> length([nil, z]) -> 41
() -> leq([z, s(nn2)]) -> 41
() -> leq([z, z]) -> 41
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 43
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 43
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 46
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 42
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 42
(leq([s(nn1), z])) -> BOT -> 42
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> z  ;  ll -> nil  ;  x -> s(s(s(z)))
})

-------------------------------------------
Step 52, which took 0.540052 s (model generation: 0.511606,  model checking: 0.028446):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, s, z>(q_gen_444) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, s>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474, q_gen_506},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_506) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_461) -> q_gen_452
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_440) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_506
<cons>(q_gen_461, q_gen_473) -> q_gen_506
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_506) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_473) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<cons, s>(q_gen_474, q_gen_506) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_506) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 42
() -> length([nil, z]) -> 42
() -> leq([z, s(nn2)]) -> 42
() -> leq([z, z]) -> 42
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 43
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 46
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 46
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 43
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 43
(leq([s(nn1), z])) -> BOT -> 43
}
Sat witness: Found: ((append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]), {
_eb -> cons(s(s(z)), cons(s(s(z)), cons(z, nil)))  ;  h1 -> s(z)  ;  l2 -> cons(z, cons(z, cons(s(s(z)), nil)))  ;  t1 -> cons(s(s(z)), cons(s(z), nil))
})

-------------------------------------------
Step 53, which took 0.724282 s (model generation: 0.715263,  model checking: 0.009019):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_456, q_gen_457, q_gen_458},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<s, s, s>(q_gen_458) -> q_gen_458
<s, s, z>(q_gen_444) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<s, z, z>(q_gen_457) -> q_gen_458
<z, s, s>(q_gen_444) -> q_gen_458
<z, s, z>(q_gen_457) -> q_gen_458
<z, z, s>(q_gen_457) -> q_gen_458
<z, z, z>() -> q_gen_458
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468, q_gen_473, q_gen_474, q_gen_506},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_506) -> q_gen_440
<nil>() -> q_gen_440
<s>(q_gen_461) -> q_gen_452
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_452, q_gen_465) -> q_gen_473
<cons>(q_gen_461, q_gen_440) -> q_gen_473
<cons>(q_gen_461, q_gen_465) -> q_gen_473
<cons>(q_gen_452, q_gen_473) -> q_gen_506
<cons>(q_gen_461, q_gen_473) -> q_gen_506
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_441, q_gen_506) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<cons, s>(q_gen_466, q_gen_473) -> q_gen_436
<cons, s>(q_gen_474, q_gen_473) -> q_gen_436
<cons, s>(q_gen_474, q_gen_506) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_474) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_441, q_gen_473) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
<cons, s>(q_gen_466, q_gen_506) -> q_gen_468
<cons, s>(q_gen_474, q_gen_440) -> q_gen_468
<cons, s>(q_gen_474, q_gen_465) -> q_gen_468
<s, s>(q_gen_466) -> q_gen_474
<z, s>(q_gen_461) -> q_gen_474
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 43
() -> length([nil, z]) -> 43
() -> leq([z, s(nn2)]) -> 43
() -> leq([z, z]) -> 43
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 46
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 46
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 46
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 44
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 44
(leq([s(nn1), z])) -> BOT -> 44
}
Sat witness: Found: ((append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]), {
_nb -> s(s(s(s(z))))  ;  _ob -> cons(z, cons(z, cons(s(z), nil)))  ;  _pb -> s(s(s(z)))  ;  l1 -> cons(z, cons(z, nil))  ;  l2 -> nil
})

-------------------------------------------
Step 54, which took 0.712011 s (model generation: 0.709316,  model checking: 0.002695):

Model:
|_
{
append -> 
{{{
Q={q_gen_437, q_gen_443, q_gen_444, q_gen_455, q_gen_456, q_gen_457, q_gen_458, q_gen_463, q_gen_501},
Q_f={q_gen_437},
Delta=
{
<cons>(q_gen_457, q_gen_456) -> q_gen_456
<nil>() -> q_gen_456
<s>(q_gen_457) -> q_gen_457
<z>() -> q_gen_457
<cons, cons>(q_gen_444, q_gen_443) -> q_gen_443
<nil, nil>() -> q_gen_443
<s, s>(q_gen_444) -> q_gen_444
<s, z>(q_gen_457) -> q_gen_444
<z, s>(q_gen_457) -> q_gen_444
<z, z>() -> q_gen_444
<cons, cons>(q_gen_444, q_gen_463) -> q_gen_463
<nil, cons>(q_gen_457, q_gen_456) -> q_gen_463
<cons, cons, cons>(q_gen_458, q_gen_455) -> q_gen_437
<cons, cons, cons>(q_gen_501, q_gen_437) -> q_gen_437
<cons, nil, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, cons, cons>(q_gen_444, q_gen_443) -> q_gen_437
<nil, nil, nil>() -> q_gen_437
<cons, cons, cons>(q_gen_458, q_gen_437) -> q_gen_455
<cons, cons, cons>(q_gen_501, q_gen_455) -> q_gen_455
<cons, nil, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, cons, cons>(q_gen_444, q_gen_463) -> q_gen_455
<nil, nil, cons>(q_gen_457, q_gen_456) -> q_gen_455
<s, s, s>(q_gen_501) -> q_gen_458
<s, z, s>(q_gen_444) -> q_gen_458
<z, z, z>() -> q_gen_458
<s, s, s>(q_gen_458) -> q_gen_501
<s, s, z>(q_gen_444) -> q_gen_501
<s, z, z>(q_gen_457) -> q_gen_501
<z, s, s>(q_gen_444) -> q_gen_501
<z, s, z>(q_gen_457) -> q_gen_501
<z, z, s>(q_gen_457) -> q_gen_501
}

Datatype: <natlist, natlist, natlist>
Convolution form: left
}}}
  ;  length -> 
{{{
Q={q_gen_436, q_gen_440, q_gen_441, q_gen_452, q_gen_461, q_gen_465, q_gen_466, q_gen_468},
Q_f={q_gen_436},
Delta=
{
<cons>(q_gen_452, q_gen_465) -> q_gen_440
<cons>(q_gen_461, q_gen_465) -> q_gen_440
<nil>() -> q_gen_440
<z>() -> q_gen_452
<s>(q_gen_452) -> q_gen_461
<s>(q_gen_461) -> q_gen_461
<cons>(q_gen_452, q_gen_440) -> q_gen_465
<cons>(q_gen_461, q_gen_440) -> q_gen_465
<cons, s>(q_gen_441, q_gen_440) -> q_gen_436
<cons, s>(q_gen_466, q_gen_465) -> q_gen_436
<nil, z>() -> q_gen_436
<s, s>(q_gen_466) -> q_gen_441
<s, z>(q_gen_452) -> q_gen_441
<s, z>(q_gen_461) -> q_gen_441
<z, s>(q_gen_461) -> q_gen_441
<z, z>() -> q_gen_441
<s, s>(q_gen_441) -> q_gen_466
<z, s>(q_gen_452) -> q_gen_466
<cons, s>(q_gen_441, q_gen_465) -> q_gen_468
<cons, s>(q_gen_466, q_gen_440) -> q_gen_468
}

Datatype: <natlist, nat>
Convolution form: left
}}}
  ;  leq -> 
{{{
Q={q_gen_433, q_gen_435, q_gen_469},
Q_f={q_gen_433},
Delta=
{
<s>(q_gen_435) -> q_gen_435
<z>() -> q_gen_435
<s, s>(q_gen_433) -> q_gen_433
<z, s>(q_gen_435) -> q_gen_433
<z, z>() -> q_gen_433
<s, s>(q_gen_469) -> q_gen_469
<s, z>(q_gen_435) -> q_gen_469
}

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

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

Teacher's answer:
New clause system:
{
() -> append([nil, l2, l2]) -> 44
() -> length([nil, z]) -> 44
() -> leq([z, s(nn2)]) -> 44
() -> leq([z, z]) -> 44
(append([l1, l2, _ob]) /\ length([_ob, _pb]) /\ length([l1, _nb])) -> leq([_nb, _pb]) -> 46
(append([t1, l2, _eb])) -> append([cons(h1, t1), l2, cons(h1, _eb)]) -> 46
(length([ll, _jb])) -> length([cons(x, ll), s(_jb)]) -> 49
(leq([nn1, nn2])) -> leq([s(nn1), s(nn2)]) -> 45
(leq([s(nn1), s(nn2)])) -> leq([nn1, nn2]) -> 45
(leq([s(nn1), z])) -> BOT -> 45
}
Sat witness: Found: ((length([ll, _jb])) -> length([cons(x, ll), s(_jb)]), {
_jb -> s(s(s(z)))  ;  ll -> cons(z, nil)  ;  x -> z
})

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