Solving ../../benchmarks/smtlib/true/isaplanner_prop59.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: { nat -> {s, z} ; natlist -> {cons, nil} } definition: { (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) } eq_natlist(_iya, _jya) <= append(_gya, _hya, _iya) /\ append(_gya, _hya, _jya) ) (last, F: { last(cons(y, nil), y) <= True last(nil, z) <= True last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) } eq_nat(_mya, _nya) <= last(_lya, _mya) /\ last(_lya, _nya) ) } properties: { eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) } over-approximation: {append, last} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Solving took 60.433705 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(s(s(z)), nil)), s(s(z))) <= True last(cons(s(z), cons(s(z), cons(z, nil))), z) <= True last(cons(s(z), cons(z, cons(s(z), nil))), s(z)) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ last(cons(s(s(z)), nil), z) False <= append(cons(s(z), cons(z, cons(s(z), nil))), nil, cons(s(z), nil)) /\ last(cons(s(z), cons(z, cons(s(z), nil))), z) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) append(cons(z, cons(s(z), cons(z, nil))), nil, cons(z, cons(z, nil))) <= append(cons(s(z), cons(z, nil)), nil, cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, cons(s(z), nil))), nil, cons(z, cons(s(z), cons(z, nil)))) <= append(cons(z, cons(s(z), nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, cons(s(z), nil)), nil, cons(z, cons(z, nil))) append(cons(s(z), cons(z, cons(z, nil))), nil, cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, cons(z, nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(z, cons(z, cons(s(z), nil))), s(s(z))) <= last(cons(z, cons(s(z), nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) False <= last(nil, s(z)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_6(x_0_0) /\ _r_6(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= _r_6(x_0_0) _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= _r_6(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006039 s (model generation: 0.005981, model checking: 0.000058): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; last -> [ last : { } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } last(cons(y, nil), y) <= True : Yes: { y -> z } last(nil, z) <= True : Yes: { } append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : No: () last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 1, which took 0.006708 s (model generation: 0.006630, model checking: 0.000078): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True last(cons(z, nil), z) <= True last(nil, z) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; last -> [ last : { last(cons(x_0_0, x_0_1), z) <= True last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_qbgk_0, _qbgk_1) } last(cons(y, nil), y) <= True : Yes: { y -> s(_rbgk_0) } last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> nil ; l2 -> nil ; t1 -> nil } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : No: () last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 2, which took 0.009083 s (model generation: 0.008984, model checking: 0.000099): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, nil), z) <= True last(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 } ] ; last -> [ last : { last(cons(x_0_0, x_0_1), s(x_1_0)) <= True last(cons(x_0_0, x_0_1), z) <= True last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(_vbgk_0, _vbgk_1) ; l2 -> cons(_wbgk_0, _wbgk_1) ; t1 -> nil } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(_gcgk_0, _gcgk_1) ; _pya -> z ; _qya -> s(_icgk_0) ; xs -> cons(_jcgk_0, _jcgk_1) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 3, which took 0.017312 s (model generation: 0.017189, model checking: 0.000123): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= last(cons(z, nil), 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 } ] ; last -> [ last : { _r_1(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0) last(cons(x_0_0, x_0_1), z) <= True last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(_tcgk_0, _tcgk_1) ; _pya -> z ; _qya -> s(_vcgk_0) ; xs -> cons(s(_ycgk_0), _wcgk_1) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(_xcgk_0) ; x2 -> s(_ycgk_0) ; y -> z } ------------------------------------------- Step 4, which took 0.056166 s (model generation: 0.055882, model checking: 0.000284): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_3(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0) last(cons(x_0_0, x_0_1), z) <= True last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> nil ; h1 -> s(_pegk_0) ; l2 -> nil ; t1 -> nil } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(_pdgk_0, cons(_qegk_0, _qegk_1)) ; _pya -> s(_qdgk_0) ; _qya -> z ; xs -> cons(z, _sdgk_1) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 5, which took 0.069946 s (model generation: 0.069439, model checking: 0.000507): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0) last(cons(x_0_0, x_0_1), z) <= True last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_ehgk_0), _bggk_1) ; _pya -> s(_cggk_0) ; _qya -> z ; xs -> cons(s(_dhgk_0), _eggk_1) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(_nggk_0) ; x2 -> z ; x3 -> cons(s(_fhgk_0), _chgk_1) ; y -> z } ------------------------------------------- Step 6, which took 0.078113 s (model generation: 0.077626, model checking: 0.000487): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), nil), z) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_2(s(x_0_0)) <= True _r_3(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _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_0) _r_2(s(x_0_0)) <= True _r_3(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_gkgk_0), cons(s(_kkgk_0), _ikgk_1)) ; _pya -> s(_aigk_0) ; _qya -> z ; xs -> cons(z, _cigk_1) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> z ; x2 -> z ; y -> s(_nkgk_0) } ------------------------------------------- Step 7, which took 0.138794 s (model generation: 0.138196, model checking: 0.000598): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), nil), z) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(z, nil) <= True _r_3(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(s(x_0_0)) <= True _r_4(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(s(_lpgk_0), _tkgk_1) ; h1 -> z ; l2 -> nil ; t1 -> cons(s(_epgk_0), _vkgk_1) } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_epgk_0), cons(_ipgk_0, _ipgk_1)) ; _pya -> s(_nngk_0) ; _qya -> z ; xs -> cons(s(_epgk_0), cons(_ipgk_0, _ipgk_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 8, which took 0.210504 s (model generation: 0.209533, model checking: 0.000971): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) /\ last(cons(s(z), cons(z, nil)), s(z)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), nil), z) False <= last(cons(z, nil), 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_3(x_0_0) _r_1(nil, nil) <= True _r_3(s(x_0_0)) <= True _r_4(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(s(x_0_0)) <= True _r_4(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(_rpgk_0, nil) ; l2 -> nil ; t1 -> cons(z, nil) } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_cvgk_0), nil) ; _pya -> s(_xtgk_0) ; _qya -> z ; xs -> cons(z, nil) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 9, which took 0.249148 s (model generation: 0.246938, model checking: 0.002210): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) /\ last(cons(s(z), cons(z, nil)), s(z)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), nil), z) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(z) <= True _r_4(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(cons(x_0_0, x_0_1)) <= True _r_3(z) <= True _r_4(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_1(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(z, nil) ; h1 -> s(_dkhk_0) ; l2 -> nil ; t1 -> cons(z, _ibhk_1) } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_nkhk_0), _tghk_1) ; _pya -> s(z) ; _qya -> s(s(_lkhk_0)) ; xs -> cons(s(_nkhk_0), nil) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 10, which took 0.279487 s (model generation: 0.278536, model checking: 0.000951): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), cons(z, nil)), s(z)) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_3(z) <= True _r_4(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(z) <= True _r_4(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : Yes: { y -> s(s(_gqhk_0)) } last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_sqhk_0), nil) ; _pya -> s(z) ; _qya -> z ; xs -> cons(s(_pqhk_0), cons(_qqhk_0, _qqhk_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : No: () ------------------------------------------- Step 11, which took 0.323213 s (model generation: 0.319092, model checking: 0.004121): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), cons(z, nil)), s(z)) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(s(x_0_0)) <= True _r_4(s(x_0_0)) <= _r_3(x_0_0) _r_4(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_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_3(x_0_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(s(x_0_0)) <= True _r_4(s(x_0_0)) <= _r_3(x_0_0) _r_4(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_1_0) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_1(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(z, cons(_flik_0, _flik_1)) ; _pya -> s(s(_klik_0)) ; _qya -> z ; xs -> cons(z, cons(_flik_0, _flik_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(s(z)) ; x2 -> z ; x3 -> cons(_glik_0, _glik_1) ; y -> s(z) } ------------------------------------------- Step 12, which took 0.403203 s (model generation: 0.398200, model checking: 0.005003): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), cons(z, nil)), s(z)) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(s(z), cons(z, cons(z, nil))), s(s(z))) <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(s(x_0_0)) <= True _r_4(s(x_0_0)) <= _r_3(x_0_0) _r_4(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_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_3(x_0_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(s(x_0_0)) <= True _r_4(s(x_0_0)) <= _r_3(x_0_0) _r_4(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_1(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(z, nil) ; _pya -> z ; _qya -> s(s(_bijk_0)) ; xs -> cons(z, nil) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(s(z)) ; x2 -> z ; x3 -> nil ; y -> s(z) } ------------------------------------------- Step 13, which took 0.708965 s (model generation: 0.707516, model checking: 0.001449): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= last(cons(s(z), cons(z, nil)), s(z)) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(s(z), cons(z, cons(z, nil))), s(s(z))) <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True _r_3(nil) <= True _r_4(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)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_0) /\ _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_2(x_0_0, x_2_0) /\ _r_4(x_0_1) /\ _r_4(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), z) <= True _r_2(s(x_0_0), s(x_1_0)) <= True _r_2(z, z) <= True _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= True _r_5(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0, x_1_0) /\ _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(z, cons(_tqjk_0, _tqjk_1)) ; _pya -> s(z) ; _qya -> z ; xs -> cons(z, cons(_tqjk_0, _tqjk_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(s(_irjk_0)) ; x2 -> s(_jrjk_0) ; x3 -> cons(_sqjk_0, _sqjk_1) ; y -> z } ------------------------------------------- Step 14, which took 0.972704 s (model generation: 0.968801, model checking: 0.003903): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(s(z), cons(z, cons(z, nil))), s(s(z))) <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, cons(z, nil)), s(z)) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= 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)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _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)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(z) <= True _r_5(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ _r_4(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_0) /\ _r_5(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ _r_5(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1) /\ _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_xfkk_0), cons(_zfkk_0, _zfkk_1)) ; _pya -> z ; _qya -> s(z) ; xs -> cons(z, cons(_zfkk_0, _zfkk_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> z ; x2 -> s(_wgkk_0) ; x3 -> cons(_xgkk_0, _xgkk_1) ; y -> z } ------------------------------------------- Step 15, which took 1.044330 s (model generation: 1.040103, model checking: 0.004227): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, cons(z, nil)), nil, cons(s(z), cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(s(z), cons(z, cons(z, nil))), s(s(z))) <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, cons(z, nil)), s(z)) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_5(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _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_1(x_0_0, x_2_0) /\ _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)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(z) <= True _r_5(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ _r_4(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_0) /\ _r_5(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ _r_5(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1) /\ _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_dxkk_0), cons(s(_ovkk_0), _rvkk_1)) ; _pya -> s(z) ; _qya -> z ; xs -> cons(s(_cxkk_0), cons(_nvkk_0, _nvkk_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(s(s(_ovkk_0))) ; x2 -> s(_ovkk_0) ; x3 -> nil ; y -> z } ------------------------------------------- Step 16, which took 1.157224 s (model generation: 1.151550, model checking: 0.005674): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, cons(z, nil)), nil, cons(s(z), cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, nil))) /\ last(cons(z, cons(z, nil)), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(s(z), cons(z, cons(z, nil))), s(s(z))) <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, cons(z, nil)), s(z)) /\ last(cons(z, cons(z, nil)), z) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= 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)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _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_1(x_0_0, x_2_0) /\ _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_0, x_2_0) append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= 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)) <= True _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(z) <= True _r_5(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_0) /\ _r_5(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ _r_5(x_0_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_1) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1) /\ _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(z, _iblk_1) ; h1 -> s(_mrlk_0) ; l2 -> cons(z, _jblk_1) ; t1 -> nil } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(z, cons(_vrlk_0, cons(_tqlk_0, _tqlk_1))) ; _pya -> s(_xflk_0) ; _qya -> z ; xs -> cons(z, nil) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> z ; x2 -> z ; x3 -> nil ; y -> z } ------------------------------------------- Step 17, which took 7.373483 s (model generation: 7.371699, model checking: 0.001784): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), 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_3(x_0_0, x_1_0) _r_1(nil, nil) <= True _r_3(s(x_0_0), s(x_1_0)) <= True _r_3(z, z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_2(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) _r_2(cons(x_0_0, x_0_1), z) <= _r_6(x_0_0) _r_2(nil, z) <= True _r_3(s(x_0_0), s(x_1_0)) <= True _r_3(z, z) <= True _r_4(cons(x_0_0, x_0_1)) <= True _r_5(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_4(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_6(x_0_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_0, x_1_0) /\ _r_5(x_0_0) /\ _r_6(x_1_0) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_ocmk_0), nil) ; _pya -> s(z) ; _qya -> z ; xs -> cons(s(s(_mcmk_0)), nil) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(s(_lcmk_0)) ; x2 -> s(s(_mcmk_0)) ; y -> s(z) } ------------------------------------------- Step 18, which took 19.248602 s (model generation: 19.245660, model checking: 0.002942): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(s(s(z)), nil)), s(s(z))) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ last(cons(s(s(z)), nil), z) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, s(x_1_0)) <= True _r_1(nil, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_6(x_0_0) _r_2(s(x_0_0), z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_6(x_0_0) /\ _r_6(x_2_0) /\ last(x_0_1, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_0, x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_1) /\ _r_5(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, s(x_1_0)) <= True last(nil, z) <= True } ] ; last -> [ last : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, s(x_1_0)) <= True _r_1(nil, z) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_6(x_0_0) _r_2(s(x_0_0), z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_0, x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_3(x_0_1) /\ _r_5(x_0_0) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, s(x_1_0)) <= True last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : No: () eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> nil ; _pya -> z ; _qya -> s(_tpmk_0) ; xs -> nil } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(z) ; x2 -> z ; x3 -> cons(s(_jsmk_0), _dsmk_1) ; y -> s(_armk_0) } ------------------------------------------- Step 19, which took 3.282793 s (model generation: 3.277110, model checking: 0.005683): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(s(s(z)), nil)), s(s(z))) <= True last(cons(s(z), cons(z, cons(s(z), nil))), s(z)) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ last(cons(s(s(z)), nil), z) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) False <= last(nil, 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_5(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) /\ _r_6(x_1_0) _r_1(nil, nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_5(s(x_0_0)) <= True _r_6(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, 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_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_6(x_0_0) /\ _r_6(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_5(x_0_0) _r_2(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1) _r_2(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) _r_2(nil, s(x_1_0)) <= True _r_2(nil, z) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_5(s(x_0_0)) <= True _r_6(z) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_3(x_0_1) /\ _r_6(x_1_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_4(x_0_0) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) /\ _r_5(x_0_0) /\ _r_6(x_1_0) last(cons(x_0_0, x_0_1), z) <= _r_3(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_6(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(s(_ounk_0), cons(_vunk_0, _vunk_1)) ; h1 -> z ; l2 -> nil ; t1 -> cons(z, cons(s(_hunk_0), _uunk_1)) } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(z, cons(_qynk_0, _qynk_1)) ; _pya -> z ; _qya -> s(z) ; xs -> cons(z, cons(s(_qvnk_0), _pynk_1)) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> s(s(_svnk_0)) ; x2 -> z ; x3 -> cons(s(_junk_0), _rvnk_1) ; y -> z } ------------------------------------------- Step 20, which took 5.604950 s (model generation: 5.596534, model checking: 0.008416): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(s(s(z)), nil)), s(s(z))) <= True last(cons(s(z), cons(z, cons(s(z), nil))), s(z)) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ last(cons(s(s(z)), nil), z) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, cons(s(z), nil))), nil, cons(z, cons(s(z), cons(z, nil)))) <= append(cons(z, cons(s(z), nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, cons(s(z), nil)), nil, cons(z, cons(z, nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(z, cons(z, cons(s(z), nil))), s(s(z))) <= last(cons(z, cons(s(z), nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) False <= last(nil, s(z)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_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_6(x_0_0) /\ _r_6(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_1) /\ _r_4(x_2_1) /\ _r_5(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(s(x_0_0), z) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(s(_zmpk_0), cons(z, _popk_1)) ; h1 -> s(_zmpk_0) ; l2 -> nil ; t1 -> cons(_wsok_0, cons(z, nil)) } eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) : Yes: { _oya -> cons(s(_dppk_0), nil) ; _pya -> s(z) ; _qya -> z ; xs -> cons(s(_cnpk_0), cons(z, cons(s(_cnpk_0), _xmpk_1))) } last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) : Yes: { _kya -> z ; x2 -> s(_lmpk_0) ; x3 -> cons(z, _rmpk_1) ; y -> s(_lmpk_0) } ------------------------------------------- Step 21, which took 18.178892 s (model generation: 18.172531, model checking: 0.006361): Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(s(s(z)), nil)), s(s(z))) <= True last(cons(s(z), cons(s(z), cons(z, nil))), z) <= True last(cons(s(z), cons(z, cons(s(z), nil))), s(z)) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ last(cons(s(s(z)), nil), z) False <= append(cons(s(z), cons(z, cons(s(z), nil))), nil, cons(s(z), nil)) /\ last(cons(s(z), cons(z, cons(s(z), nil))), z) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, cons(s(z), nil))), nil, cons(z, cons(s(z), cons(z, nil)))) <= append(cons(z, cons(s(z), nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, cons(s(z), nil)), nil, cons(z, cons(z, nil))) append(cons(s(z), cons(z, cons(z, nil))), nil, cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, cons(z, nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(z, cons(z, cons(s(z), nil))), s(s(z))) <= last(cons(z, cons(s(z), nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) False <= last(nil, s(z)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_6(x_0_0) /\ _r_6(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= _r_6(x_0_0) _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= _r_6(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () last(cons(y, nil), y) <= True : No: () last(nil, z) <= True : No: () append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) : Yes: { _fya -> cons(z, _mwpk_1) ; h1 -> z ; l2 -> nil ; t1 -> cons(s(_hcrk_0), cons(z, _kdrk_1)) } Total time: 60.433705 Learner time: 59.363730 Teacher time: 0.055929 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 last(cons(y, nil), y) <= True -> 0 last(nil, z) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _fya)) <= append(t1, l2, _fya) -> 0 eq_nat(_pya, _qya) <= append(xs, nil, _oya) /\ last(_oya, _pya) /\ last(xs, _qya) -> 0 last(cons(y, cons(x2, x3)), _kya) <= last(cons(x2, x3), _kya) -> 0 } Accumulated learning constraints: { append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(z), nil)) <= True append(cons(z, cons(s(z), nil)), nil, cons(z, cons(s(z), nil))) <= True append(cons(z, cons(z, nil)), nil, cons(z, cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True last(cons(s(s(z)), nil), s(s(z))) <= True last(cons(s(z), cons(s(s(z)), nil)), s(s(z))) <= True last(cons(s(z), cons(s(z), cons(z, nil))), z) <= True last(cons(s(z), cons(z, cons(s(z), nil))), s(z)) <= True last(cons(s(z), cons(z, nil)), z) <= True last(cons(s(z), nil), s(z)) <= True last(cons(z, cons(s(z), cons(z, nil))), z) <= True last(cons(z, cons(s(z), nil)), s(z)) <= True last(cons(z, cons(z, cons(s(z), nil))), s(z)) <= True last(cons(z, cons(z, nil)), z) <= True last(cons(z, nil), z) <= True last(nil, z) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ last(cons(s(s(z)), nil), z) False <= append(cons(s(z), cons(z, cons(s(z), nil))), nil, cons(s(z), nil)) /\ last(cons(s(z), cons(z, cons(s(z), nil))), z) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(s(z), cons(z, nil)), nil, cons(s(z), nil)) append(cons(z, cons(s(z), cons(z, nil))), nil, cons(z, cons(z, nil))) <= append(cons(s(z), cons(z, nil)), nil, cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, cons(s(z), nil))), nil, cons(z, cons(s(z), cons(z, nil)))) <= append(cons(z, cons(s(z), nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, cons(s(z), nil)), nil, cons(z, cons(z, nil))) append(cons(s(z), cons(z, cons(z, nil))), nil, cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, cons(z, nil)), nil, cons(s(z), cons(z, nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(s(z), nil))) /\ last(cons(s(z), cons(s(z), nil)), s(z)) False <= append(cons(z, nil), nil, cons(s(z), nil)) False <= append(cons(z, nil), nil, cons(z, cons(z, cons(z, nil)))) /\ last(cons(z, cons(z, cons(z, nil))), s(z)) last(cons(z, cons(s(z), cons(z, nil))), s(s(z))) <= last(cons(s(z), cons(z, nil)), s(s(z))) False <= last(cons(s(z), cons(z, nil)), s(z)) last(cons(z, cons(s(z), nil)), s(s(s(z)))) <= last(cons(s(z), nil), s(s(s(z)))) False <= last(cons(s(z), nil), s(s(z))) False <= last(cons(s(z), nil), z) last(cons(z, cons(z, cons(s(z), nil))), s(s(z))) <= last(cons(z, cons(s(z), nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(s(z))) False <= last(cons(z, cons(z, nil)), s(z)) False <= last(cons(z, nil), s(s(z))) False <= last(cons(z, nil), s(z)) False <= last(nil, s(z)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_6(x_0_0) /\ _r_6(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; last -> [ last : { _r_1(s(x_0_0), s(x_1_0)) <= _r_6(x_0_0) _r_1(s(x_0_0), z) <= True _r_1(z, s(x_1_0)) <= _r_6(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= True last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_0, x_1_0) /\ _r_4(x_0_1) last(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_4(x_0_1) last(cons(x_0_0, x_0_1), z) <= _r_5(x_0_0) last(nil, z) <= True } ] -- Equality automata are defined for: {nat, natlist} _|