Solving ../../benchmarks/smtlib/true/isaplanner_prop80.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: { (take, F: { take(s(u), nil, nil) <= True take(z, y, nil) <= True take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) } eq_eltlist(_ypa, _zpa) <= take(_wpa, _xpa, _ypa) /\ take(_wpa, _xpa, _zpa) ) (minus, F: { minus(s(u), z, s(u)) <= True minus(z, y, z) <= True minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) } eq_nat(_dqa, _eqa) <= minus(_bqa, _cqa, _dqa) /\ minus(_bqa, _cqa, _eqa) ) (length, F: { length(nil, z) <= True length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) } eq_nat(_hqa, _iqa) <= length(_gqa, _hqa) /\ length(_gqa, _iqa) ) (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) } eq_eltlist(_mqa, _nqa) <= append(_kqa, _lqa, _mqa) /\ append(_kqa, _lqa, _nqa) ) } properties: { eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) } over-approximation: {append, length, minus, take} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Solving took 60.972416 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, cons(b, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ minus(s(s(z)), z, s(z)) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), nil, nil) /\ take(s(z), cons(b, cons(b, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= minus(s(s(z)), s(z), z) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, nil) <= True _r_3(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_3(nil, cons(x_1_0, x_1_1)) <= True _r_4(a, a) <= True _r_4(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1, x_2_1) /\ _r_3(x_1_1, x_2_1) /\ _r_4(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_4(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_4(x_1_0, x_2_0) append(nil, 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 minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True 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 } ] ; take -> [ take : { _r_4(a, a) <= True _r_4(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006228 s (model generation: 0.006130, model checking: 0.000098): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; length -> [ length : { } ] ; minus -> [ minus : { } ] ; take -> [ take : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } length(nil, z) <= True : Yes: { } minus(s(u), z, s(u)) <= True : Yes: { } minus(z, y, z) <= True : Yes: { y -> z } take(s(u), nil, nil) <= True : Yes: { } take(z, y, nil) <= True : Yes: { y -> nil } eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : No: () append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 1, which took 0.007215 s (model generation: 0.007104, model checking: 0.000111): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True length(nil, z) <= True minus(s(z), z, s(z)) <= True minus(z, z, z) <= True take(s(z), nil, nil) <= True take(z, nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(nil, 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 } ] ; take -> [ take : { take(s(x_0_0), nil, nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_wclp_0, _wclp_1) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : Yes: { y -> s(_xclp_0) } take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : Yes: { y -> cons(_yclp_0, _yclp_1) } eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : No: () append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> nil ; l2 -> nil ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : Yes: { _fqa -> z ; ll -> nil } minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : Yes: { _aqa -> z ; u -> z ; x2 -> z } take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : Yes: { _vpa -> nil ; u -> z ; x3 -> nil } ------------------------------------------- Step 2, which took 0.012262 s (model generation: 0.011425, model checking: 0.000837): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, 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 } ] ; take -> [ take : { take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(_qdlp_0, _qdlp_1) ; _pqa -> cons(b, _rdlp_1) ; _qqa -> cons(_sdlp_0, _sdlp_1) ; _rqa -> s(_tdlp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(a, _wdlp_1) ; n -> s(_xdlp_0) ; xs -> cons(_ydlp_0, _ydlp_1) ; ys -> nil } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(_eflp_0, _eflp_1) ; l2 -> cons(_fflp_0, _fflp_1) ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : Yes: { _aqa -> s(_hflp_0) ; u -> s(_iflp_0) ; x2 -> z } take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 3, which took 0.026690 s (model generation: 0.026035, model checking: 0.000655): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(a) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(_sglp_0, _sglp_1) ; _pqa -> cons(a, nil) ; _qqa -> cons(a, _uglp_1) ; _rqa -> s(_vglp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(_yglp_0, cons(_eklp_0, _eklp_1)) ; n -> s(_zglp_0) ; xs -> cons(_ahlp_0, _ahlp_1) ; ys -> cons(_bhlp_0, _bhlp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : Yes: { _vpa -> nil ; u -> z ; x2 -> b ; x3 -> nil } ------------------------------------------- Step 4, which took 0.052709 s (model generation: 0.051864, model checking: 0.000845): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(a, a) <= True _r_1(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, _qklp_1) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, _sklp_1) ; _rqa -> s(_tklp_0) ; _sqa -> s(_uklp_0) ; _tqa -> cons(b, _vklp_1) ; _uqa -> cons(_wklp_0, cons(_hplp_0, _hplp_1)) ; n -> s(_xklp_0) ; xs -> cons(b, _yklp_1) ; ys -> cons(b, _zklp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(_colp_0, nil) ; l2 -> nil ; t1 -> cons(_eolp_0, _eolp_1) } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 5, which took 0.068120 s (model generation: 0.067317, model checking: 0.000803): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(a, a) <= True _r_1(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(_aulp_0, _aulp_1)) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, _oqlp_1) ; _rqa -> s(_pqlp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(_sqlp_0, cons(_iulp_0, _iulp_1)) ; n -> s(_tqlp_0) ; xs -> cons(b, _uqlp_1) ; ys -> cons(_vqlp_0, _vqlp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 6, which took 0.066696 s (model generation: 0.065916, model checking: 0.000780): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, _vxlp_1) ; _pqa -> cons(b, nil) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(_zxlp_0) ; _tqa -> cons(b, _aylp_1) ; _uqa -> cons(_bylp_0, cons(_jzlp_0, _jzlp_1)) ; n -> s(_cylp_0) ; xs -> nil ; ys -> cons(b, _eylp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(_iylp_0, _iylp_1) ; h1 -> b ; l2 -> cons(_jylp_0, _jylp_1) ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 7, which took 0.091392 s (model generation: 0.090411, model checking: 0.000981): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) /\ append(nil, cons(b, nil), cons(b, nil)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(a, a) <= True _r_1(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(_nemp_0, _nemp_1)) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, _xzlp_1) ; _rqa -> s(_yzlp_0) ; _sqa -> s(_zzlp_0) ; _tqa -> cons(b, _aamp_1) ; _uqa -> cons(_bamp_0, cons(_efmp_0, _efmp_1)) ; n -> s(_camp_0) ; xs -> cons(b, _damp_1) ; ys -> cons(b, _eamp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 8, which took 0.082874 s (model generation: 0.081943, model checking: 0.000931): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) /\ append(nil, cons(b, nil), cons(b, nil)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_2(a, a) <= True _r_2(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(_ckmp_0, _ckmp_1)) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, _ngmp_1) ; _rqa -> s(_ogmp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(b, cons(_skmp_0, _skmp_1)) ; n -> s(_sgmp_0) ; xs -> cons(b, _tgmp_1) ; ys -> cons(a, _ugmp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(b, _jjmp_1) ; l2 -> cons(b, _kjmp_1) ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 9, which took 0.107551 s (model generation: 0.106578, model checking: 0.000973): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) /\ append(nil, cons(b, nil), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, nil)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, cons(_hrmp_0, _hrmp_1)) ; _qqa -> cons(b, nil) ; _rqa -> s(_jnmp_0) ; _sqa -> s(_knmp_0) ; _tqa -> nil ; _uqa -> cons(_mnmp_0, nil) ; n -> s(_nnmp_0) ; xs -> cons(b, nil) ; ys -> nil } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 10, which took 0.109665 s (model generation: 0.108730, model checking: 0.000935): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) /\ append(nil, cons(b, nil), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, nil)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_2(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, cons(_oxmp_0, _oxmp_1)) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(_zump_0) ; _tqa -> cons(b, nil) ; _uqa -> cons(_bvmp_0, nil) ; n -> s(_cvmp_0) ; xs -> nil ; ys -> cons(b, nil) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 11, which took 0.104303 s (model generation: 0.103442, model checking: 0.000861): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) /\ append(nil, cons(b, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) /\ append(nil, cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, nil)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_2(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, cons(_vdnp_0, _vdnp_1)) ; _qqa -> cons(b, nil) ; _rqa -> s(_rzmp_0) ; _sqa -> s(_szmp_0) ; _tqa -> nil ; _uqa -> cons(b, nil) ; n -> s(_vzmp_0) ; xs -> cons(b, nil) ; ys -> nil } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 12, which took 0.111020 s (model generation: 0.109392, model checking: 0.001628): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, 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 take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) /\ append(nil, cons(b, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) /\ append(nil, cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, nil)) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(a) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, _kenp_1) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(a, nil) ; _rqa -> s(_sknp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(a, _vknp_1) ; n -> s(_wknp_0) ; xs -> cons(b, _xknp_1) ; ys -> cons(b, _yknp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : Yes: { _vpa -> cons(a, _mxnp_1) ; u -> s(_nxnp_0) ; x2 -> b ; x3 -> cons(_oxnp_0, _oxnp_1) } ------------------------------------------- Step 13, which took 0.155099 s (model generation: 0.153413, model checking: 0.001686): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, nil) ; _rqa -> s(_nznp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(a, nil) ; n -> s(_rznp_0) ; xs -> cons(b, nil) ; ys -> cons(_tznp_0, _tznp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : Yes: { _vpa -> nil ; u -> z ; x3 -> cons(_mdop_0, _mdop_1) } ------------------------------------------- Step 14, which took 0.181125 s (model generation: 0.179747, model checking: 0.001378): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ length(cons(b, nil), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_2(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, nil) ; _rqa -> s(_ygop_0) ; _sqa -> s(_zgop_0) ; _tqa -> cons(b, nil) ; _uqa -> cons(b, cons(_lnop_0, _lnop_1)) ; n -> s(_chop_0) ; xs -> cons(b, nil) ; ys -> cons(b, nil) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 15, which took 0.745569 s (model generation: 0.744278, model checking: 0.001291): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ length(cons(b, nil), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ length(cons(b, nil), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= length(cons(b, nil), s(z)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) append(nil, nil, nil) <= True } ] ; length -> [ length : { _r_3(a) <= True length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0) length(nil, z) <= True } ] ; minus -> [ minus : { 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(a, a) <= True _r_1(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(_bvop_0, _bvop_1)) ; _pqa -> cons(b, _zqop_1) ; _qqa -> cons(a, _arop_1) ; _rqa -> s(_brop_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(a, _erop_1) ; n -> s(_frop_0) ; xs -> cons(a, _grop_1) ; ys -> cons(_hrop_0, _hrop_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : Yes: { _fqa -> z ; ll -> nil ; x -> b } minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 16, which took 0.866773 s (model generation: 0.865815, model checking: 0.000958): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, _qzop_1) ; _pqa -> cons(b, nil) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(_uzop_0) ; _tqa -> cons(b, _vzop_1) ; _uqa -> cons(b, cons(_gcpp_0, _gcpp_1)) ; n -> s(_xzop_0) ; xs -> nil ; ys -> cons(b, _zzop_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : Yes: { _aqa -> s(s(_qbpp_0)) ; u -> s(_wapp_0) ; x2 -> z } take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 17, which took 0.636100 s (model generation: 0.634872, model checking: 0.001228): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, 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_1_0, x_2_0) append(nil, 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), z) <= True _r_1(z, s(x_1_0)) <= 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), s(x_2_0)) <= _r_1(x_1_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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, cons(_rlpp_0, _rlpp_1)) ; _qqa -> cons(b, nil) ; _rqa -> s(_shpp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(b, nil) ; n -> s(_whpp_0) ; xs -> cons(b, nil) ; ys -> nil } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : Yes: { _aqa -> s(s(_skpp_0)) ; u -> s(z) ; x2 -> s(_njpp_0) } take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 18, which took 0.860396 s (model generation: 0.857019, model checking: 0.003377): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_3(a, a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a, a) <= True _r_2(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, cons(_veqp_0, _veqp_1)) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, nil) ; _rqa -> s(_mppp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(a, nil) ; n -> s(z) ; xs -> cons(b, nil) ; ys -> cons(b, nil) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(_ycqp_0, nil) ; h1 -> b ; l2 -> cons(b, cons(_veqp_0, _veqp_1)) ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 19, which took 0.864902 s (model generation: 0.863727, model checking: 0.001175): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(nil, cons(x_1_0, x_1_1)) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, nil) ; _rqa -> s(_ypqp_0) ; _sqa -> s(_zpqp_0) ; _tqa -> nil ; _uqa -> cons(a, nil) ; n -> s(_cqqp_0) ; xs -> cons(b, nil) ; ys -> nil } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(a, cons(_yvqp_0, _yvqp_1)) ; l2 -> cons(_esqp_0, _esqp_1) ; t1 -> cons(a, nil) } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 20, which took 1.388758 s (model generation: 1.387481, model checking: 0.001277): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, cons(x_1_0, x_1_1)) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_2(x_1_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(_ubrp_0) ; _tqa -> cons(b, nil) ; _uqa -> cons(a, nil) ; n -> s(_xbrp_0) ; xs -> nil ; ys -> cons(b, nil) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 21, which took 1.272309 s (model generation: 1.270988, model checking: 0.001321): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(nil, cons(x_1_0, x_1_1)) <= True _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) <= True _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, 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_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _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) <= True _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True take(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_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(_gyrp_0, _gyrp_1)) ; _pqa -> cons(b, cons(_hyrp_0, _hyrp_1)) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(_ynrp_0) ; _tqa -> cons(b, nil) ; _uqa -> cons(b, nil) ; n -> s(_borp_0) ; xs -> nil ; ys -> cons(b, cons(_fyrp_0, _fyrp_1)) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(a, cons(_asrp_0, _asrp_1)) ; l2 -> cons(a, cons(_yrrp_0, _yrrp_1)) ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 22, which took 3.600409 s (model generation: 3.598707, model checking: 0.001702): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, 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_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(_vnsp_0, _vnsp_1)) ; _pqa -> cons(b, nil) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(s(z)) ; _tqa -> cons(b, cons(b, nil)) ; _uqa -> cons(b, cons(_xnsp_0, _xnsp_1)) ; n -> s(z) ; xs -> nil ; ys -> cons(b, cons(b, nil)) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 23, which took 2.527071 s (model generation: 2.521062, model checking: 0.006009): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ take(s(z), cons(b, cons(a, nil)), cons(b, nil)) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, a) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_1_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, a) <= True _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0, x_2_0) take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_0) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(a, _ustp_1) ; _pqa -> cons(a, cons(_aiup_0, _aiup_1)) ; _qqa -> cons(a, nil) ; _rqa -> s(_xstp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(a, nil) ; n -> s(_bttp_0) ; xs -> cons(b, _cttp_1) ; ys -> cons(b, _dttp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, nil) ; t1 -> nil } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : Yes: { _vpa -> nil ; u -> z ; x2 -> b ; x3 -> cons(_zdup_0, _zdup_1) } ------------------------------------------- Step 24, which took 3.477883 s (model generation: 3.476101, model checking: 0.001782): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_0) _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, 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_1_0, x_2_0) append(nil, 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), 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), 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 } ] ; take -> [ take : { _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(b, nil) ; _rqa -> s(z) ; _sqa -> s(z) ; _tqa -> cons(b, nil) ; _uqa -> cons(b, cons(_czup_0, _czup_1)) ; n -> s(s(_zyup_0)) ; xs -> cons(b, nil) ; ys -> cons(b, nil) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : Yes: { _aqa -> s(_rmup_0) ; u -> s(s(_eoup_0)) ; x2 -> s(z) } take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 25, which took 6.055731 s (model generation: 6.053904, model checking: 0.001827): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), s(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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_0) _r_2(nil, nil) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, 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_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(b, nil)) ; _pqa -> cons(b, cons(b, nil)) ; _qqa -> nil ; _rqa -> z ; _sqa -> s(z) ; _tqa -> cons(b, nil) ; _uqa -> cons(b, nil) ; n -> s(s(z)) ; xs -> nil ; ys -> cons(b, cons(b, _gqvp_1)) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 26, which took 8.579380 s (model generation: 8.576210, model checking: 0.003170): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), s(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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ minus(s(s(z)), z, s(z)) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), nil, nil) /\ take(s(z), cons(b, cons(b, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_1) _r_1(nil, nil) <= True _r_2(a, cons(x_1_0, x_1_1)) <= True _r_2(a, nil) <= True _r_2(b, cons(x_1_0, x_1_1)) <= True _r_3(a, a) <= True _r_3(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_0_0, x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_1) /\ _r_3(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0, x_2_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_3(a, a) <= True _r_3(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_nqvp_0, cons(b, nil)) } length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, cons(b, nil)) ; _pqa -> cons(b, cons(b, nil)) ; _qqa -> cons(b, nil) ; _rqa -> s(_yuvp_0) ; _sqa -> z ; _tqa -> nil ; _uqa -> cons(b, nil) ; n -> s(s(z)) ; xs -> cons(b, nil) ; ys -> cons(b, _evvp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(b, nil) ; l2 -> nil ; t1 -> cons(b, nil) } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 27, which took 1.747386 s (model generation: 1.734540, model checking: 0.012846): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), s(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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) /\ take(z, cons(b, nil), nil) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ minus(s(s(z)), z, s(z)) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), nil, nil) /\ take(s(z), cons(b, cons(b, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= minus(s(s(z)), s(z), z) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) /\ take(z, cons(b, nil), nil) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_1(nil, nil) <= True _r_2(a) <= True _r_3(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_2(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) append(nil, 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), 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)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] ; take -> [ take : { _r_2(a) <= True _r_3(b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_0) take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : Yes: { y -> cons(b, _oaxp_1) } eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) : Yes: { _oqa -> cons(b, nil) ; _pqa -> cons(b, nil) ; _qqa -> cons(a, _tnxp_1) ; _rqa -> s(_unxp_0) ; _sqa -> s(_vnxp_0) ; _tqa -> cons(a, nil) ; _uqa -> cons(a, nil) ; n -> s(z) ; xs -> cons(b, _znxp_1) ; ys -> cons(a, _aoxp_1) } append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) : Yes: { _jqa -> cons(a, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> cons(_rhbq_0, _rhbq_1) } length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : No: () take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) : No: () ------------------------------------------- Step 28, which took 26.104044 s (model generation: 26.102649, model checking: 0.001395): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), s(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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, cons(b, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ minus(s(s(z)), z, s(z)) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), nil, nil) /\ take(s(z), cons(b, cons(b, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= minus(s(s(z)), s(z), z) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, nil) <= True _r_3(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_3(nil, cons(x_1_0, x_1_1)) <= True _r_4(a, a) <= True _r_4(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1, x_2_1) /\ _r_3(x_1_1, x_2_1) /\ _r_4(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_4(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_4(x_1_0, x_2_0) append(nil, 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 minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True 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 } ] ; take -> [ take : { _r_4(a, a) <= True _r_4(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () minus(s(u), z, s(u)) <= True : Yes: { u -> s(_ywbq_0) } minus(z, y, z) <= True : No: () take(s(u), nil, nil) <= True : No: () take(z, y, nil) <= True : No: () length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) : No: () minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) : Yes: { _aqa -> z ; u -> z ; x2 -> s(_wvbq_0) } Total time: 60.972416 Learner time: 59.856800 Teacher time: 0.052860 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 take(s(u), nil, nil) <= True -> 0 take(z, y, nil) <= True -> 0 eq_eltlist(_pqa, _uqa) <= append(_qqa, _tqa, _uqa) /\ append(xs, ys, _oqa) /\ length(xs, _rqa) /\ minus(n, _rqa, _sqa) /\ take(_sqa, ys, _tqa) /\ take(n, _oqa, _pqa) /\ take(n, xs, _qqa) -> 0 append(cons(h1, t1), l2, cons(h1, _jqa)) <= append(t1, l2, _jqa) -> 0 length(cons(x, ll), s(_fqa)) <= length(ll, _fqa) -> 0 minus(s(u), s(x2), _aqa) <= minus(u, x2, _aqa) -> 0 take(s(u), cons(x2, x3), cons(x2, _vpa)) <= take(u, x3, _vpa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True length(cons(a, nil), s(z)) <= True length(cons(b, nil), s(z)) <= True length(nil, z) <= True minus(s(s(s(z))), s(s(z)), 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 take(s(s(z)), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True take(s(z), cons(a, cons(a, nil)), cons(a, nil)) <= True take(s(z), cons(a, nil), cons(a, nil)) <= True take(s(z), cons(b, cons(a, nil)), cons(b, nil)) <= True take(s(z), cons(b, nil), cons(b, nil)) <= True take(s(z), nil, nil) <= True take(z, cons(a, nil), nil) <= True take(z, cons(b, nil), nil) <= True take(z, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ take(s(z), cons(a, nil), cons(a, cons(a, nil))) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ append(cons(b, nil), nil, cons(a, nil)) False <= append(cons(b, nil), cons(b, nil), cons(b, nil)) /\ take(s(z), cons(b, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) /\ minus(s(z), s(z), s(z)) False <= append(cons(b, nil), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ minus(s(z), z, s(s(z))) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ minus(s(s(z)), z, s(z)) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), nil, nil) /\ take(s(z), cons(b, cons(b, nil)), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= minus(s(s(z)), s(z), z) /\ take(s(s(z)), cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ take(s(s(z)), cons(b, nil), cons(b, nil)) minus(s(s(z)), s(s(z)), s(s(z))) <= minus(s(z), s(z), s(s(z))) minus(s(s(z)), s(z), s(s(z))) <= minus(s(z), z, s(s(z))) False <= take(s(z), cons(a, nil), cons(b, nil)) False <= take(s(z), cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= take(s(z), cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil, nil) <= True _r_3(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_3(nil, cons(x_1_0, x_1_1)) <= True _r_4(a, a) <= True _r_4(b, b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1, x_2_1) /\ _r_3(x_1_1, x_2_1) /\ _r_4(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1, x_2_1) /\ _r_4(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_4(x_1_0, x_2_0) append(nil, 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 minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True 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 } ] ; take -> [ take : { _r_4(a, a) <= True _r_4(b, b) <= True take(s(x_0_0), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0, x_2_0) /\ take(x_0_0, x_1_1, x_2_1) take(s(x_0_0), nil, nil) <= True take(z, cons(x_1_0, x_1_1), nil) <= True take(z, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _|