Solving ../../benchmarks/smtlib/true/append_length_commutative.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: { (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) } eq_eltlist(_aoa, _boa) <= append(_yna, _zna, _aoa) /\ append(_yna, _zna, _boa) ) (length, F: { length(nil, z) <= True length(cons(x, ll), s(_coa)) <= length(ll, _coa) } eq_nat(_eoa, _foa) <= length(_doa, _eoa) /\ length(_doa, _foa) ) } properties: { eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) } over-approximation: {append, length} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Solving took 59.337378 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, cons(a, nil)))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil)))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, nil)) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1) /\ _r_3(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_1_1) /\ _r_3(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_2_1) /\ _r_2(x_0_1) /\ _r_2(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_3(x_0_1) /\ _r_3(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_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006328 s (model generation: 0.006241, model checking: 0.000087): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; length -> [ length : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } length(nil, z) <= True : Yes: { } eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : No: () append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 1, which took 0.006153 s (model generation: 0.006093, model checking: 0.000060): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True length(nil, z) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; length -> [ length : { length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_yekc_0, _yekc_1) } length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : No: () append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> nil ; l2 -> nil ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : Yes: { _coa -> z ; ll -> nil } ------------------------------------------- Step 2, which took 0.009889 s (model generation: 0.009721, model checking: 0.000168): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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 } 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 } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_kfkc_0, _kfkc_1) ; _hoa -> s(z) ; _ioa -> cons(_mfkc_0, _mfkc_1) ; _joa -> s(s(_yfkc_0)) ; l1 -> nil ; l2 -> cons(_pfkc_0, _pfkc_1) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_qfkc_0, _qfkc_1) ; l2 -> cons(_rfkc_0, _rfkc_1) ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 3, which took 0.025005 s (model generation: 0.024757, model checking: 0.000248): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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 False <= length(cons(a, nil), s(s(z))) } 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)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_zfkc_0, nil) ; _hoa -> s(z) ; _ioa -> cons(_bgkc_0, cons(_fhkc_0, nil)) ; _joa -> s(s(z)) ; l1 -> cons(_dgkc_0, _dgkc_1) ; l2 -> cons(_egkc_0, _egkc_1) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 4, which took 0.019886 s (model generation: 0.019703, model checking: 0.000183): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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 False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ length(cons(a, cons(a, nil)), s(s(z))) False <= length(cons(a, nil), s(s(z))) } 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 : { _r_1(z) <= True length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : No: () append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : Yes: { _coa -> s(z) ; ll -> cons(_eikc_0, _eikc_1) } ------------------------------------------- Step 5, which took 0.020260 s (model generation: 0.020074, model checking: 0.000186): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(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_1(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)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_uikc_0, cons(_ujkc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_wikc_0, nil) ; _joa -> s(z) ; l1 -> nil ; l2 -> cons(_zikc_0, _zikc_1) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 6, which took 0.036499 s (model generation: 0.036241, model checking: 0.000258): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(nil) <= 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_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_akkc_0, cons(_dlkc_0, _dlkc_1)) } length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_hkkc_0, cons(_glkc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_jkkc_0, nil) ; _joa -> s(z) ; l1 -> cons(_lkkc_0, _lkkc_1) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 7, which took 0.040511 s (model generation: 0.040161, model checking: 0.000350): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } 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(nil, 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_2(x_0_1, x_2_1) 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)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_tlkc_0, cons(_cnkc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_vlkc_0, cons(_bnkc_0, cons(_xnkc_0, nil))) ; _joa -> s(s(s(z))) ; l1 -> cons(_xlkc_0, cons(_ankc_0, _ankc_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_fmkc_0, cons(_gnkc_0, _gnkc_1)) ; l2 -> cons(_gmkc_0, _gmkc_1) ; t1 -> cons(_hmkc_0, nil) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 8, which took 0.066639 s (model generation: 0.066293, model checking: 0.000346): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, 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, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _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)) <= _r_1(x_2_1) 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)) <= _r_1(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_wokc_0, cons(_eqkc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_yokc_0, nil) ; _joa -> s(z) ; l1 -> nil ; l2 -> cons(_bpkc_0, cons(_bqkc_0, _bqkc_1)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_lpkc_0, nil) ; l2 -> nil ; t1 -> cons(_npkc_0, _npkc_1) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 9, which took 0.075320 s (model generation: 0.074934, model checking: 0.000386): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } 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)) <= _r_2(x_0_1, x_1_1) _r_2(nil, nil) <= 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), nil, cons(x_2_0, x_2_1)) <= _r_2(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_1, x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_mqkc_0, cons(_wrkc_0, cons(_btkc_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_oqkc_0, cons(_yrkc_0, nil)) ; _joa -> s(s(z)) ; l1 -> cons(_qqkc_0, nil) ; l2 -> cons(_rqkc_0, nil) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_hrkc_0, cons(_qskc_0, nil)) ; l2 -> cons(_irkc_0, cons(_pskc_0, nil)) ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 10, which took 0.091854 s (model generation: 0.090797, model checking: 0.001057): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _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)) <= _r_1(x_0_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_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_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_mtkc_0, cons(_ozkc_0, cons(_szkc_0, _szkc_1))) } length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_ttkc_0, cons(_ealc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_vtkc_0, nil) ; _joa -> s(z) ; l1 -> cons(_xtkc_0, cons(_pzkc_0, nil)) ; l2 -> cons(_ytkc_0, _ytkc_1) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_rxkc_0, cons(_lalc_0, nil)) ; l2 -> cons(_sxkc_0, nil) ; t1 -> cons(_txkc_0, cons(_szkc_0, _szkc_1)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 11, which took 0.140003 s (model generation: 0.138701, model checking: 0.001302): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_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_1) /\ _r_2(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_2_1) /\ _r_2(x_0_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_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_mclc_0, cons(_bjlc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_oclc_0, nil) ; _joa -> s(z) ; l1 -> cons(_qclc_0, cons(_nilc_0, nil)) ; l2 -> cons(_rclc_0, cons(_nilc_0, nil)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 12, which took 0.151567 s (model generation: 0.150226, model checking: 0.001341): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _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)) <= _r_1(x_0_1) /\ _r_2(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_1_1) /\ _r_2(x_0_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_2_1) /\ _r_2(x_0_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_sklc_0, cons(_lvlc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_uklc_0, nil) ; _joa -> s(z) ; l1 -> cons(_wklc_0, nil) ; l2 -> cons(_xklc_0, cons(_dulc_0, nil)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_cslc_0, nil) ; l2 -> cons(_dslc_0, cons(_dulc_0, nil)) ; t1 -> cons(_eslc_0, nil) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 13, which took 0.223338 s (model generation: 0.218135, model checking: 0.005203): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_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_1) /\ _r_1(x_1_1) /\ _r_2(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_1) /\ _r_1(x_2_1) /\ _r_2(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_1(x_1_1) /\ _r_1(x_2_1) /\ _r_2(x_0_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_0_1) /\ _r_2(x_1_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_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_txlc_0, cons(_wbnc_0, cons(_lbnc_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_vxlc_0, nil) ; _joa -> s(z) ; l1 -> cons(_xxlc_0, cons(_kanc_0, nil)) ; l2 -> cons(_yxlc_0, nil) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 14, which took 0.734482 s (model generation: 0.733860, model checking: 0.000622): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_2(nil) <= True _r_3(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_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), 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)) <= _r_3(x_1_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) _r_1(nil, z) <= True _r_2(nil) <= True length(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_vdnc_0, cons(_jhnc_0, nil)) ; _hoa -> s(s(_khnc_0)) ; _ioa -> cons(_xdnc_0, nil) ; _joa -> s(z) ; l1 -> cons(_zdnc_0, cons(_bhnc_0, _bhnc_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : Yes: { _coa -> s(s(_ygnc_0)) ; ll -> cons(_tgnc_0, cons(_xgnc_0, nil)) } ------------------------------------------- Step 15, which took 0.480045 s (model generation: 0.479415, model checking: 0.000630): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) _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)) <= _r_3(x_1_1) _r_3(nil) <= 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) 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_1, x_2_1) 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)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_vhnc_0, cons(_aknc_0, cons(_umnc_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_xhnc_0, cons(_zjnc_0, nil)) ; _joa -> s(s(z)) ; l1 -> cons(_zhnc_0, cons(_yjnc_0, _yjnc_1)) ; l2 -> cons(_ainc_0, _ainc_1) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 16, which took 0.500908 s (model generation: 0.499064, model checking: 0.001844): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } 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_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= 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) 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_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_2_1) /\ _r_3(x_1_1) 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(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(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) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_ennc_0, cons(_xvnc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_gnnc_0, cons(_vvnc_0, cons(_kwnc_0, nil))) ; _joa -> s(s(s(z))) ; l1 -> cons(_innc_0, cons(_wvnc_0, _wvnc_1)) ; l2 -> cons(_jnnc_0, cons(_uvnc_0, _uvnc_1)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 17, which took 0.619254 s (model generation: 0.617254, model checking: 0.002000): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True _r_1(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_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_1, x_1_1, x_2_1) /\ _r_2(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_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_mync_0, cons(_jeoc_0, cons(_neoc_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_oync_0, nil) ; _joa -> s(z) ; l1 -> cons(_qync_0, nil) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_gboc_0, cons(_rfoc_0, cons(_xdoc_0, nil))) ; l2 -> cons(_hboc_0, cons(_qfoc_0, nil)) ; t1 -> cons(_iboc_0, nil) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 18, which took 0.910199 s (model generation: 0.906461, model checking: 0.003738): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } 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(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_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_1, x_1_1) /\ _r_3(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_1_1, x_2_1) /\ _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_3(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_1) /\ _r_2(x_2_1) /\ _r_3(x_0_1) 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) /\ _r_2(x_1_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) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_kgoc_0, cons(_dyoc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_mgoc_0, nil) ; _joa -> s(z) ; l1 -> cons(_ogoc_0, cons(_rxoc_0, cons(_qxoc_0, nil))) ; l2 -> cons(_pgoc_0, cons(_sxoc_0, nil)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_ploc_0, cons(_xyoc_0, nil)) ; l2 -> cons(_qloc_0, cons(_jzoc_0, cons(_gzoc_0, nil))) ; t1 -> cons(_rloc_0, cons(_izoc_0, nil)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 19, which took 2.301288 s (model generation: 2.288332, model checking: 0.012956): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } 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(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_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_1_1, x_2_1) /\ _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_3(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_0_1) /\ _r_2(x_1_1) /\ _r_3(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_1) /\ _r_2(x_2_1) /\ _r_3(x_0_1) 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) /\ _r_3(x_1_1) /\ _r_3(x_2_1) 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) /\ _r_2(x_1_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) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_uapc_0, cons(_jsqc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_wapc_0, cons(_isqc_0, cons(_xsqc_0, cons(_etqc_0, nil)))) ; _joa -> s(s(s(s(z)))) ; l1 -> cons(_yapc_0, nil) ; l2 -> cons(_zapc_0, nil) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_srqc_0, cons(_tvqc_0, nil)) ; l2 -> cons(_trqc_0, cons(_svqc_0, cons(_jvqc_0, nil))) ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 20, which took 3.464657 s (model generation: 3.461258, model checking: 0.003399): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1) /\ _r_3(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_1_1) /\ _r_3(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_2_1) /\ _r_2(x_0_1) /\ _r_2(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_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_kzqc_0, cons(_jorc_0, nil)) ; _hoa -> s(s(z)) ; _ioa -> cons(_mzqc_0, nil) ; _joa -> s(z) ; l1 -> cons(_ozqc_0, cons(_tnrc_0, cons(_rnrc_0, nil))) ; l2 -> cons(_pzqc_0, cons(_tnrc_0, cons(_rnrc_0, nil))) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_umrc_0, cons(_worc_0, nil)) ; l2 -> nil ; t1 -> cons(_wmrc_0, cons(_cprc_0, nil)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 21, which took 5.237865 s (model generation: 5.235693, model checking: 0.002172): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(nil, nil) <= True _r_2(nil) <= True _r_3(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_1(x_0_1, x_2_1) /\ _r_3(x_1_1) /\ _r_3(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_1_1, x_2_1) /\ _r_3(x_0_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_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) 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_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(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, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> nil ; _hoa -> z ; _ioa -> cons(_ssrc_0, nil) ; _joa -> s(z) ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_kbsc_0, nil) ; l2 -> nil ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 22, which took 2.310444 s (model generation: 2.307212, model checking: 0.003232): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1) /\ _r_3(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_1_1) /\ _r_3(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_2_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_phsc_0, nil) ; _hoa -> s(z) ; _ioa -> cons(_rhsc_0, cons(_bvsc_0, cons(_pvsc_0, nil))) ; _joa -> s(s(s(z))) ; l1 -> cons(_thsc_0, cons(_kusc_0, cons(_gusc_0, nil))) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_xjsc_0, cons(_nwsc_0, cons(_jwsc_0, nil))) ; l2 -> cons(_yjsc_0, nil) ; t1 -> cons(_zjsc_0, cons(_pwsc_0, nil)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 23, which took 3.310697 s (model generation: 3.305711, model checking: 0.004986): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1) /\ _r_2(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_1(x_1_1) /\ _r_3(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_2_1) /\ _r_2(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_3(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_wxsc_0, cons(_nxtc_0, cons(_vwtc_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_yxsc_0, cons(_oxtc_0, nil)) ; _joa -> s(s(z)) ; l1 -> cons(_aysc_0, nil) ; l2 -> cons(_bysc_0, cons(_pvtc_0, nil)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_mftc_0, cons(_jytc_0, cons(_lxtc_0, cons(_tvtc_0, cons(_pvtc_0, nil))))) ; l2 -> cons(_nftc_0, cons(_mytc_0, cons(_eytc_0, cons(_tvtc_0, cons(_pvtc_0, nil))))) ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 24, which took 5.318034 s (model generation: 5.305639, model checking: 0.012395): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(nil) <= 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) /\ _r_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_1(x_1_1) /\ _r_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_1(x_2_1) /\ _r_2(x_0_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_2_1) /\ _r_2(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_2_1) /\ _r_3(x_0_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_leuc_0, cons(_ogwc_0, cons(_ifwc_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_neuc_0, cons(_pgwc_0, nil)) ; _joa -> s(s(z)) ; l1 -> cons(_peuc_0, cons(_vewc_0, cons(_wewc_0, nil))) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_urvc_0, nil) ; l2 -> cons(_vrvc_0, cons(_jhwc_0, cons(_wewc_0, nil))) ; t1 -> nil } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 25, which took 4.359263 s (model generation: 4.334525, model checking: 0.024738): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_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_1) /\ _r_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_1(x_1_1) /\ _r_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_1(x_2_1) /\ _r_3(x_0_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_2_1) /\ _r_3(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_0_1) /\ _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_wiwc_0, cons(_voyc_0, cons(_cryc_0, cons(_gpyc_0, cons(_ppyc_0, nil))))) ; _hoa -> s(s(s(s(s(z))))) ; _ioa -> cons(_yiwc_0, cons(_uoyc_0, cons(_dryc_0, nil))) ; _joa -> s(s(s(z))) ; l1 -> cons(_ajwc_0, _ajwc_1) ; l2 -> cons(_bjwc_0, cons(_wnyc_0, cons(_aoyc_0, nil))) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : No: () length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 26, which took 6.247655 s (model generation: 6.237256, model checking: 0.010399): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(nil) <= 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) /\ _r_3(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_2_1) /\ _r_2(x_0_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_2_1) /\ _r_2(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_0_1) /\ _r_3(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_2_1) /\ _r_3(x_0_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_uuyc_0, cons(_eqad_0, cons(_iqad_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_wuyc_0, nil) ; _joa -> s(z) ; l1 -> cons(_yuyc_0, cons(_soad_0, nil)) ; l2 -> cons(_zuyc_0, cons(_road_0, cons(_soad_0, nil))) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_zaad_0, nil) ; l2 -> cons(_abad_0, _abad_1) ; t1 -> cons(_bbad_0, cons(_bsad_0, nil)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 27, which took 4.944549 s (model generation: 4.932404, model checking: 0.012145): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, nil)) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= 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) /\ _r_2(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_1) /\ _r_3(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_1_1) /\ _r_2(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_2_1) /\ _r_3(x_0_1) /\ _r_3(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_0_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_evad_0, cons(_oycd_0, cons(_xwcd_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_gvad_0, nil) ; _joa -> s(z) ; l1 -> cons(_ivad_0, _ivad_1) ; l2 -> cons(_jvad_0, cons(_ftcd_0, nil)) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_nccd_0, nil) ; l2 -> cons(_occd_0, cons(_aucd_0, nil)) ; t1 -> cons(_pccd_0, cons(_hxcd_0, nil)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 28, which took 6.333890 s (model generation: 6.310675, model checking: 0.023215): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, nil)) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= 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) /\ _r_1(x_1_1) /\ _r_3(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_1) /\ _r_2(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_1_1) /\ _r_2(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_2_1) /\ _r_2(x_0_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_2_1) /\ _r_3(x_0_1) /\ _r_3(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_0_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_gldd_0, cons(_cjgd_0, cons(_uggd_0, cons(_ifgd_0, nil)))) ; _hoa -> s(s(s(s(z)))) ; _ioa -> cons(_ildd_0, nil) ; _joa -> s(z) ; l1 -> nil ; l2 -> cons(_lldd_0, nil) } append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) : Yes: { _xna -> cons(_vsed_0, cons(_sjgd_0, cons(_njgd_0, nil))) ; l2 -> cons(_wsed_0, cons(_qegd_0, nil)) ; t1 -> cons(_xsed_0, cons(_thgd_0, nil)) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () ------------------------------------------- Step 29, which took 7.206542 s (model generation: 7.144830, model checking: 0.061712): Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, nil)) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1) /\ _r_3(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_1_1) /\ _r_3(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_2_1) /\ _r_2(x_0_1) /\ _r_2(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_3(x_0_1) /\ _r_3(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_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () length(nil, z) <= True : No: () eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) : Yes: { _goa -> cons(_logd_0, cons(_alkd_0, cons(_wrid_0, nil))) ; _hoa -> s(s(s(z))) ; _ioa -> cons(_nogd_0, cons(_zkkd_0, cons(_xrid_0, cons(_oqid_0, cons(_vqid_0, nil))))) ; _joa -> s(s(s(s(s(z))))) ; l1 -> cons(_pogd_0, cons(_ykkd_0, cons(_iqid_0, cons(_eqid_0, nil)))) ; l2 -> cons(_qogd_0, nil) } length(cons(x, ll), s(_coa)) <= length(ll, _coa) : No: () Total time: 59.337378 Learner time: 55.001666 Teacher time: 0.191359 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 length(nil, z) <= True -> 0 eq_nat(_hoa, _joa) <= append(l1, l2, _goa) /\ append(l2, l1, _ioa) /\ length(_goa, _hoa) /\ length(_ioa, _joa) -> 0 append(cons(h1, t1), l2, cons(h1, _xna)) <= append(t1, l2, _xna) -> 0 length(cons(x, ll), s(_coa)) <= length(ll, _coa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) <= True append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= True 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, cons(a, nil)), cons(a, 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, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True length(cons(a, cons(a, cons(a, nil))), s(s(s(z)))) <= True length(cons(a, cons(a, nil)), s(s(z))) <= True length(cons(a, nil), s(z)) <= True length(nil, z) <= True False <= append(cons(a, cons(a, cons(a, cons(a, nil)))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil)))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, nil)) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, cons(a, nil))), cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) /\ length(cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), s(s(s(s(s(z)))))) False <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, cons(a, nil))))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(cons(a, nil), cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))))) <= append(nil, cons(a, cons(a, cons(a, cons(a, cons(a, nil))))), cons(a, cons(a, cons(a, cons(a, cons(a, nil)))))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) append(cons(a, nil), cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, cons(a, cons(a, nil))))) /\ length(cons(a, cons(a, cons(a, cons(a, nil)))), s(s(s(s(z))))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, nil, cons(a, nil)) False <= length(cons(a, nil), s(s(z))) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1) /\ _r_3(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_1_1) /\ _r_3(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_2_1) /\ _r_2(x_0_1) /\ _r_2(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_3(x_0_1) /\ _r_3(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_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; length -> [ length : { length(cons(x_0_0, x_0_1), s(x_1_0)) <= length(x_0_1, x_1_0) length(nil, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _|