Solving ../../benchmarks/smtlib/true/isaplanner_prop19.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: Some(60.) (sec) Teacher_type: Checks all clauses every time Approximation method: remove every clause that can be safely removed Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} ; nat -> {s, z} } definition: { (drop, F: { drop(s(u), nil, nil) <= True drop(z, l, l) <= True drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) } eq_eltlist(_bza, _cza) <= drop(_zya, _aza, _bza) /\ drop(_zya, _aza, _cza) ) (length, F: { length(nil, z) <= True length(cons(x, ll), s(_dza)) <= length(ll, _dza) } eq_nat(_fza, _gza) <= length(_eza, _fza) /\ length(_eza, _gza) ) (minus, F: { minus(s(u), z, s(u)) <= True minus(z, y, z) <= True minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) } eq_nat(_kza, _lza) <= minus(_iza, _jza, _kza) /\ minus(_iza, _jza, _lza) ) } properties: { eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) } over-approximation: {drop, length, minus} under-approximation: {} Clause system for inference is: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Solving took 59.160563 seconds. Maybe: timeout during learnerLast solver state: Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(s(z))), z, s(s(s(z)))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, cons(a, nil))), nil) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) drop(s(z), cons(a, cons(a, cons(a, cons(a, nil)))), cons(a, nil)) <= drop(z, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), z) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z)))) False <= minus(s(s(z)), z, s(z)) False <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1), nil) <= _r_6(x_0_1) _r_3(s(x_0_0)) <= True _r_4(z) <= True _r_5(nil) <= True _r_6(cons(x_0_0, x_0_1)) <= _r_5(x_0_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_6(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_0_0) /\ _r_6(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0) _r_1(s(x_0_0), z) <= _r_3(x_0_0) _r_1(z, z) <= True _r_3(s(x_0_0)) <= True _r_4(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_0) /\ _r_4(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0) /\ _r_4(x_1_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_4(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005828 s (model generation: 0.005763, model checking: 0.000065): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None drop -> [ drop : { } ] ; length -> [ length : { } ] ; minus -> [ minus : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : Yes: { } drop(z, l, l) <= True : Yes: { l -> nil } length(nil, z) <= True : Yes: { } minus(s(u), z, s(u)) <= True : Yes: { } minus(z, y, z) <= True : Yes: { y -> z } eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : No: () drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 1, which took 0.008826 s (model generation: 0.007918, model checking: 0.000908): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), nil, nil) <= True drop(z, nil, nil) <= True length(nil, z) <= True minus(s(z), z, s(z)) <= True minus(z, z, z) <= True } Current best model: |_ name: None drop -> [ drop : { drop(s(x_0_0), nil, nil) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(nil, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : Yes: { l -> cons(_zqse_0, _zqse_1) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : Yes: { y -> s(_arse_0) } eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : No: () drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> nil ; u -> z ; x3 -> nil } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : Yes: { _dza -> z ; ll -> nil } minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> z ; u -> z ; x2 -> z } ------------------------------------------- Step 2, which took 0.013461 s (model generation: 0.013324, model checking: 0.000137): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True } Current best model: |_ name: None drop -> [ drop : { drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= True length(nil, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_prse_0, _prse_1) ; _nza -> s(z) ; _oza -> s(_rrse_0) ; _pza -> s(s(_gsse_0)) ; l1 -> cons(_trse_0, _trse_1) ; n -> z } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> cons(_vrse_0, _vrse_1) ; u -> z ; x3 -> cons(_xrse_0, _xrse_1) } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> s(_yrse_0) ; u -> s(_zrse_0) ; x2 -> z } ------------------------------------------- Step 3, which took 0.018236 s (model generation: 0.017905, model checking: 0.000331): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= True length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : Yes: { u -> s(_ftse_0) } minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(_vsse_0) ; _pza -> s(_wsse_0) ; l1 -> cons(_xsse_0, _xsse_1) ; n -> s(_ysse_0) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 4, which took 0.033562 s (model generation: 0.033350, model checking: 0.000212): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= True length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(s(x_0_0), z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_mtse_0, _mtse_1) ; _nza -> s(_ntse_0) ; _oza -> s(_otse_0) ; _pza -> z ; l1 -> cons(_qtse_0, _qtse_1) ; n -> s(_rtse_0) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 5, which took 0.058809 s (model generation: 0.058544, model checking: 0.000265): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_3(cons(x_0_0, x_0_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= True length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_2(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(s(_owse_0)) ; _pza -> s(z) ; l1 -> cons(_jvse_0, _jvse_1) ; n -> s(_kvse_0) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 6, which took 0.060499 s (model generation: 0.060094, model checking: 0.000405): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_3(cons(x_0_0, x_0_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0), z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(s(z)) ; _pza -> s(z) ; l1 -> cons(_gxse_0, cons(_myse_0, nil)) ; n -> s(_hxse_0) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> s(s(_jyse_0)) ; u -> s(s(_iyse_0)) ; x2 -> z } ------------------------------------------- Step 7, which took 0.083025 s (model generation: 0.082622, model checking: 0.000403): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, cons(a, nil)), nil) /\ length(cons(a, cons(a, nil)), s(s(z))) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_3(cons(x_0_0, x_0_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= True drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { _r_1(z) <= True length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_tyse_0, _tyse_1) ; _nza -> s(z) ; _oza -> s(z) ; _pza -> z ; l1 -> cons(_xyse_0, cons(_nate_0, _nate_1)) ; n -> s(_yyse_0) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : Yes: { _dza -> s(z) ; ll -> cons(_yzse_0, _yzse_1) } minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 8, which took 0.179747 s (model generation: 0.179444, model checking: 0.000303): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_2(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_uate_0, nil) ; _nza -> s(z) ; _oza -> s(s(z)) ; _pza -> z ; l1 -> cons(_yate_0, cons(_ycte_0, nil)) ; n -> s(_zate_0) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> nil ; u -> s(_zbte_0) ; x3 -> cons(_acte_0, nil) } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 9, which took 0.178326 s (model generation: 0.177913, model checking: 0.000413): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_3(z, cons(x_1_0, x_1_1)) <= True _r_4(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_4(z, nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_0_0, x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(s(x_0_0), z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_bdte_0, nil) ; _nza -> s(z) ; _oza -> s(s(z)) ; _pza -> s(s(_tfte_0)) ; l1 -> cons(_fdte_0, cons(_wfte_0, nil)) ; n -> s(z) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> nil ; u -> s(_jete_0) ; x3 -> nil } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> z ; u -> z ; x2 -> s(_dfte_0) } ------------------------------------------- Step 10, which took 0.205084 s (model generation: 0.204264, model checking: 0.000820): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_1(s(x_0_0), nil) <= True _r_1(z, nil) <= True _r_2(z, cons(x_1_0, x_1_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0, x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_3(s(x_0_0)) <= _r_4(x_0_0) _r_3(z) <= True _r_4(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_2_0) /\ _r_4(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_4(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_hhte_0, nil) ; _nza -> s(z) ; _oza -> s(s(z)) ; _pza -> s(s(_glte_0)) ; l1 -> cons(_lhte_0, cons(_wkte_0, nil)) ; n -> z } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> cons(_nhte_0, _nhte_1) ; u -> s(z) ; x3 -> cons(_phte_0, cons(_qkte_0, _qkte_1)) } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> z ; u -> s(z) ; x2 -> s(_gjte_0) } ------------------------------------------- Step 11, which took 0.312906 s (model generation: 0.311932, model checking: 0.000974): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(s(x_0_0)) <= True _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : Yes: { l -> cons(_nlte_0, cons(_arte_0, _arte_1)) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_gmte_0, nil) ; _nza -> s(z) ; _oza -> s(s(z)) ; _pza -> z ; l1 -> cons(_kmte_0, cons(_mrte_0, nil)) ; n -> s(s(_drte_0)) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> s(s(z)) ; u -> s(z) ; x2 -> s(_uote_0) } ------------------------------------------- Step 12, which took 0.376781 s (model generation: 0.374885, model checking: 0.001896): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0) /\ _r_3(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_4(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_1(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_otte_0, nil) ; _nza -> s(z) ; _oza -> s(s(z)) ; _pza -> z ; l1 -> cons(_stte_0, cons(_pcue_0, nil)) ; n -> s(s(s(_obue_0))) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 13, which took 0.396878 s (model generation: 0.395296, model checking: 0.001582): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) /\ minus(s(s(z)), s(s(s(z))), z) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0) /\ _r_3(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_4(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(z) ; _pza -> s(s(z)) ; l1 -> cons(_pfue_0, nil) ; n -> s(s(z)) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> nil ; u -> s(s(z)) ; x3 -> cons(_tiue_0, nil) } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> z ; u -> s(z) ; x2 -> s(s(z)) } ------------------------------------------- Step 14, which took 1.227972 s (model generation: 1.227115, model checking: 0.000857): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(s(z)), s(s(z))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_2(s(x_0_0), nil) <= True _r_2(z, nil) <= True _r_3(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_1) _r_3(z, cons(x_1_0, x_1_1)) <= True _r_4(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_4(nil, nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0, x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1, x_2_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_5(x_0_0) _r_1(z, z) <= True _r_5(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_5(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_5(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_lpue_0, nil) ; _nza -> s(z) ; _oza -> s(s(s(z))) ; _pza -> z ; l1 -> cons(_ppue_0, cons(_wtue_0, cons(_nuue_0, nil))) ; n -> s(s(z)) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 15, which took 1.217475 s (model generation: 1.216043, model checking: 0.001432): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ minus(s(s(s(z))), s(s(z)), z) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(s(z)), s(s(z))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(s(x_0_0)) <= True _r_3(z) <= True _r_4(cons(x_0_0, x_0_1)) <= True _r_5(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_5(nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_5(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_4(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_2(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0) _r_1(s(x_0_0), z) <= _r_2(x_0_0) _r_2(s(x_0_0)) <= True _r_3(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) /\ _r_3(x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(s(z)) ; _pza -> s(z) ; l1 -> cons(_ywue_0, cons(_ucve_0, nil)) ; n -> s(s(_gcve_0)) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> cons(_qyue_0, _qyue_1) ; u -> s(s(_odve_0)) ; x3 -> cons(_syue_0, nil) } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> z ; u -> s(s(s(_pdve_0))) ; x2 -> s(z) } ------------------------------------------- Step 16, which took 1.445346 s (model generation: 1.443339, model checking: 0.002007): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) /\ minus(s(s(s(z))), s(s(z)), z) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(s(z)), s(s(z))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_1) _r_2(z, cons(x_1_0, x_1_1)) <= True _r_3(s(x_0_0)) <= True _r_4(nil) <= True _r_5(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { _r_4(nil) <= True _r_5(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) /\ length(x_0_1, x_1_0) length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_5(x_0_1) /\ length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= _r_3(x_0_0) _r_1(z, z) <= True _r_3(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) /\ _r_3(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : Yes: { l -> cons(_qdve_0, cons(_ipve_0, cons(_ppve_0, _ppve_1))) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(s(z)) ; _pza -> s(s(_rpve_0)) ; l1 -> cons(_five_0, cons(_mqve_0, nil)) ; n -> s(s(_qpve_0)) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : Yes: { _dza -> s(s(z)) ; ll -> cons(_zlve_0, cons(_hqve_0, nil)) } minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 17, which took 6.214916 s (model generation: 6.214137, model checking: 0.000779): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), z) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_4(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0, x_1_1) _r_4(z, cons(x_1_0, x_1_1)) <= True _r_5(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_5(s(x_0_0), nil) <= True _r_5(z, nil) <= True _r_6(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_6(nil, nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_0_0, x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_1, x_2_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), z) <= True _r_2(z, s(x_1_0)) <= True _r_2(z, z) <= True _r_3(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_3(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_3(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : Yes: { u -> s(s(_nuve_0)) } minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> nil ; _nza -> z ; _oza -> s(s(s(z))) ; _pza -> s(z) ; l1 -> cons(_jsve_0, cons(_evve_0, cons(_ovve_0, nil))) ; n -> s(s(z)) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> s(s(s(z))) ; u -> s(s(z)) ; x2 -> z } ------------------------------------------- Step 18, which took 15.175155 s (model generation: 15.174443, model checking: 0.000712): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(s(z))), z, s(s(s(z)))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, cons(a, nil))), nil) /\ minus(s(s(s(z))), s(s(z)), s(z)) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), z) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z)))) False <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_4(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0, x_1_1) _r_4(z, cons(x_1_0, x_1_1)) <= True _r_5(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_5(s(x_0_0), nil) <= True _r_5(z, nil) <= True _r_6(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_6(nil, nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_0_0, x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_1, x_2_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(s(x_0_0), z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(z, s(x_1_0)) <= True _r_2(z, z) <= True _r_3(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_3(s(x_0_0), z) <= True _r_3(z, z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_0, x_2_0) /\ _r_3(x_0_0, x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_3(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_ixve_0, cons(_uawe_0, nil)) ; _nza -> s(s(z)) ; _oza -> s(s(z)) ; _pza -> s(z) ; l1 -> cons(_mxve_0, cons(_tawe_0, nil)) ; n -> z } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> s(z) ; u -> s(s(_obwe_0)) ; x2 -> s(z) } ------------------------------------------- Step 19, which took 10.963953 s (model generation: 10.962804, model checking: 0.001149): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(s(z))), z, s(s(s(z)))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, cons(a, nil))), nil) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), z) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z)))) False <= minus(s(s(z)), z, s(z)) False <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_3(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_1) _r_3(s(x_0_0), nil) <= True _r_3(z, nil) <= True _r_4(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0, x_1_1) _r_4(z, cons(x_1_0, x_1_1)) <= True _r_5(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_5(nil, nil) <= True drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0, x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_0_0, x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_1, x_2_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_6(x_0_0) _r_1(s(x_0_0), z) <= _r_6(x_0_0) _r_1(z, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(z, s(x_1_0)) <= True _r_2(z, z) <= True _r_6(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_6(x_0_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0, x_2_0) /\ _r_6(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0, x_2_0) /\ _r_6(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_sbwe_0, nil) ; _nza -> s(z) ; _oza -> s(s(s(z))) ; _pza -> s(s(_zgwe_0)) ; l1 -> cons(_wbwe_0, cons(_qiwe_0, cons(_siwe_0, nil))) ; n -> s(z) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : No: () length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : No: () ------------------------------------------- Step 20, which took 17.838159 s (model generation: 17.833697, model checking: 0.004462): Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(s(z))), z, s(s(s(z)))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, cons(a, nil))), nil) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), z) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z)))) False <= minus(s(s(z)), z, s(z)) False <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1), nil) <= _r_6(x_0_1) _r_3(s(x_0_0)) <= True _r_4(z) <= True _r_5(nil) <= True _r_6(cons(x_0_0, x_0_1)) <= _r_5(x_0_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_6(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_0_0) /\ _r_6(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0) _r_1(s(x_0_0), z) <= _r_3(x_0_0) _r_1(z, z) <= True _r_3(s(x_0_0)) <= True _r_4(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_0) /\ _r_4(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0) /\ _r_4(x_1_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_4(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: drop(s(u), nil, nil) <= True : No: () drop(z, l, l) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) : Yes: { _mza -> cons(_jlwe_0, cons(_dbxe_0, nil)) ; _nza -> s(s(z)) ; _oza -> s(s(z)) ; _pza -> s(z) ; l1 -> cons(_nlwe_0, cons(_jbxe_0, nil)) ; n -> s(z) } drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) : Yes: { _yya -> cons(_wpwe_0, nil) ; u -> z ; x3 -> cons(_ypwe_0, cons(_pcxe_0, cons(_taxe_0, nil))) } length(cons(x, ll), s(_dza)) <= length(ll, _dza) : No: () minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) : Yes: { _hza -> s(s(_caxe_0)) ; u -> s(s(s(_wzwe_0))) ; x2 -> s(z) } Total time: 59.160563 Learner time: 55.994832 Teacher time: 0.020112 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { drop(s(u), nil, nil) <= True -> 0 drop(z, l, l) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_nza, _pza) <= drop(n, l1, _mza) /\ length(_mza, _nza) /\ length(l1, _oza) /\ minus(_oza, n, _pza) -> 0 drop(s(u), cons(x2, x3), _yya) <= drop(u, x3, _yya) -> 0 length(cons(x, ll), s(_dza)) <= length(ll, _dza) -> 0 minus(s(u), s(x2), _hza) <= minus(u, x2, _hza) -> 0 } Accumulated learning constraints: { drop(s(s(s(z))), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) <= True drop(s(s(z)), cons(a, cons(a, nil)), nil) <= True drop(s(s(z)), cons(a, nil), nil) <= True drop(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True drop(s(z), cons(a, nil), nil) <= True drop(s(z), nil, nil) <= True drop(z, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True drop(z, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True drop(z, cons(a, nil), cons(a, nil)) <= True drop(z, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(s(z)))), s(s(z)), s(s(z))) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(s(z))), s(z), s(s(z))) <= True minus(s(s(s(z))), z, s(s(s(z)))) <= True minus(s(s(z)), s(s(s(z))), z) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= drop(s(s(s(z))), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, cons(a, cons(a, nil))), nil) False <= drop(s(s(z)), cons(a, cons(a, nil)), cons(a, nil)) False <= drop(s(s(z)), cons(a, nil), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= drop(s(z), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= drop(s(z), cons(a, cons(a, nil)), nil) False <= drop(s(z), cons(a, nil), cons(a, nil)) drop(s(z), cons(a, cons(a, cons(a, cons(a, nil)))), cons(a, nil)) <= drop(z, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= drop(z, cons(a, cons(a, nil)), cons(a, nil)) False <= length(cons(a, cons(a, nil)), s(z)) False <= length(cons(a, nil), s(s(z))) False <= minus(s(s(s(z))), s(s(z)), z) minus(s(s(s(s(z)))), s(s(z)), z) <= minus(s(s(s(z))), s(z), z) False <= minus(s(s(z)), s(s(z)), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), s(s(z))) False <= minus(s(s(z)), s(z), z) minus(s(s(s(z))), s(z), s(s(s(z)))) <= minus(s(s(z)), z, s(s(s(z)))) False <= minus(s(s(z)), z, s(z)) False <= minus(s(z), s(s(z)), s(s(z))) False <= minus(s(z), s(z), s(s(z))) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None drop -> [ drop : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1), nil) <= _r_6(x_0_1) _r_3(s(x_0_0)) <= True _r_4(z) <= True _r_5(nil) <= True _r_6(cons(x_0_0, x_0_1)) <= _r_5(x_0_1) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0) drop(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_6(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_3(x_0_0) /\ _r_6(x_1_1) drop(s(x_0_0), cons(x_1_0, x_1_1), nil) <= _r_5(x_1_1) drop(s(x_0_0), nil, nil) <= True drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) drop(z, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_1) drop(z, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), s(x_1_0)) <= _r_3(x_1_0) _r_1(s(x_0_0), z) <= _r_3(x_0_0) _r_1(z, z) <= True _r_3(s(x_0_0)) <= True _r_4(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_0) /\ _r_4(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0) /\ _r_4(x_1_0) /\ _r_4(x_2_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_4(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _|