Solving ../../benchmarks/smtlib/true/sort_reverse.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} } definition: { (leq, P: { leq(a, y) <= True leq(b, b) <= True False <= leq(b, a) } ) (insert, F: { insert(x, nil, cons(x, nil)) <= True insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) } eq_eltlist(_uea, _vea) <= insert(_sea, _tea, _uea) /\ insert(_sea, _tea, _vea) ) (sort, F: { sort(nil, nil) <= True sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) } eq_eltlist(_zea, _afa) <= sort(_yea, _afa) /\ sort(_yea, _zea) ) (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) } eq_eltlist(_efa, _ffa) <= append(_cfa, _dfa, _efa) /\ append(_cfa, _dfa, _ffa) ) (reverse, F: { reverse(nil, nil) <= True reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) } eq_eltlist(_jfa, _kfa) <= reverse(_ifa, _jfa) /\ reverse(_ifa, _kfa) ) } properties: { eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) } over-approximation: {append, insert, reverse, sort} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Solving took 59.321461 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ reverse(nil, cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, cons(a, nil)), nil) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(a, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(a, nil)) /\ sort(cons(b, cons(a, nil)), nil) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= sort(cons(b, cons(a, nil)), cons(a, nil)) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006063 s (model generation: 0.005981, model checking: 0.000082): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; insert -> [ insert : { } ] ; leq -> [ leq : { } ] ; reverse -> [ reverse : { } ] ; sort -> [ sort : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } insert(x, nil, cons(x, nil)) <= True : Yes: { x -> b } leq(a, y) <= True : Yes: { y -> b } leq(b, b) <= True : Yes: { } reverse(nil, nil) <= True : Yes: { } sort(nil, nil) <= True : Yes: { } reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : No: () ------------------------------------------- Step 1, which took 0.006955 s (model generation: 0.006853, model checking: 0.000102): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True insert(b, nil, cons(b, nil)) <= True leq(a, b) <= True leq(b, b) <= True reverse(nil, nil) <= True sort(nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; insert -> [ insert : { insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { reverse(nil, nil) <= True } ] ; sort -> [ sort : { sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_jvvxa_0, _jvvxa_1) } insert(x, nil, cons(x, nil)) <= True : Yes: { x -> a } leq(a, y) <= True : Yes: { y -> a } leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> nil ; l2 -> nil ; t1 -> nil } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : Yes: { _rea -> cons(_pvvxa_0, _pvvxa_1) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(_uvvxa_0, _uvvxa_1) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> b ; y -> b } False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : No: () ------------------------------------------- Step 2, which took 0.014194 s (model generation: 0.014002, model checking: 0.000192): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(nil, nil) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) \/ leq(b, a) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) } 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 } ] ; insert -> [ insert : { insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, a) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { reverse(nil, nil) <= True } ] ; sort -> [ sort : { sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> nil ; _hfa -> cons(_cwvxa_0, _cwvxa_1) ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(_ewvxa_0, _ewvxa_1) ; l2 -> cons(_fwvxa_0, _fwvxa_1) ; t1 -> nil } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> b } False <= leq(b, a) : Yes: { } eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : No: () ------------------------------------------- Step 3, which took 0.017801 s (model generation: 0.017670, model checking: 0.000131): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) } 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 } ] ; insert -> [ insert : { insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; sort -> [ sort : { sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, _lwvxa_1) ; _mfa -> cons(_mwvxa_0, _mwvxa_1) ; _nfa -> cons(a, _nwvxa_1) ; l -> cons(_owvxa_0, _owvxa_1) } ------------------------------------------- Step 4, which took 0.024320 s (model generation: 0.024096, model checking: 0.000224): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(b, _kxvxa_1) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(a, nil) ; _mfa -> cons(_sxvxa_0, _sxvxa_1) ; _nfa -> cons(a, cons(_eyvxa_0, _eyvxa_1)) ; l -> cons(_uxvxa_0, _uxvxa_1) } ------------------------------------------- Step 5, which took 0.026394 s (model generation: 0.026224, model checking: 0.000170): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, nil), cons(a, cons(a, nil))) /\ sort(cons(a, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, nil)) /\ sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(_kyvxa_0, _kyvxa_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, _vyvxa_1) ; _mfa -> cons(b, _wyvxa_1) ; _nfa -> cons(a, _xyvxa_1) ; l -> cons(b, _yyvxa_1) } ------------------------------------------- Step 6, which took 0.053649 s (model generation: 0.053176, model checking: 0.000473): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= reverse(cons(b, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a, a) <= True _r_1(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(b, _szvxa_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> cons(b, cons(b, nil)) ; _nfa -> cons(b, cons(b, nil)) ; l -> cons(b, nil) } ------------------------------------------- Step 7, which took 0.053841 s (model generation: 0.053312, model checking: 0.000529): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_2(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True _r_2(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> nil ; _hfa -> cons(_bcwxa_0, _bcwxa_1) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(b, nil) ; _xea -> cons(b, _ecwxa_1) ; y -> a ; z -> cons(b, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(a, nil) ; _mfa -> cons(b, cons(a, _wewxa_1)) ; _nfa -> cons(b, cons(_uewxa_0, _uewxa_1)) ; l -> cons(a, nil) } ------------------------------------------- Step 8, which took 0.069974 s (model generation: 0.069392, model checking: 0.000582): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, nil), cons(a, nil)) <= append(nil, cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_2(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> nil ; _hfa -> cons(b, _cfwxa_1) ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(a, cons(_lhwxa_0, _lhwxa_1)) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> cons(a, cons(b, nil)) ; _nfa -> cons(a, cons(b, nil)) ; l -> cons(b, nil) } ------------------------------------------- Step 9, which took 0.141567 s (model generation: 0.141027, model checking: 0.000540): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(a, nil), cons(b, nil)) <= append(nil, cons(a, nil), cons(b, nil)) reverse(cons(b, nil), cons(a, nil)) <= append(nil, cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_3(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True _r_2(nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> nil ; _hfa -> cons(b, _liwxa_1) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(_qjwxa_0, cons(_wkwxa_0, _wkwxa_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> cons(a, _ckwxa_1) ; _nfa -> cons(a, nil) ; l -> cons(b, _ekwxa_1) } ------------------------------------------- Step 10, which took 0.150771 s (model generation: 0.150369, model checking: 0.000402): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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 insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(a, nil), cons(b, nil)) <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, nil)) <= append(nil, cons(b, nil), cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), cons(b, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_3(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True _r_2(nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, _dlwxa_1) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(_hlwxa_0, _hlwxa_1) ; _hfa -> cons(_ilwxa_0, _ilwxa_1) ; h1 -> b ; t1 -> cons(a, _jlwxa_1) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(b, nil) ; _xea -> cons(_imwxa_0, cons(_pnwxa_0, _pnwxa_1)) ; y -> b ; z -> cons(b, _kmwxa_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(a, nil) ; _mfa -> cons(b, _ymwxa_1) ; _nfa -> cons(b, nil) ; l -> cons(a, _anwxa_1) } ------------------------------------------- Step 11, which took 0.191080 s (model generation: 0.189214, model checking: 0.001866): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(a) <= True _r_3(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) 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_2(x_1_0) /\ _r_2(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_2(a) <= True _r_3(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_2(a) <= True _r_3(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) /\ _r_2(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(a) <= True _r_3(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_2(x_0_0) /\ _r_2(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(b, _vowxa_1) ; _hfa -> cons(b, _wowxa_1) ; h1 -> a ; t1 -> cons(b, _xowxa_1) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(b, _fqwxa_1) ; l2 -> cons(b, _gqwxa_1) ; t1 -> nil } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : Yes: { _rea -> cons(b, _mqwxa_1) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(b, cons(_rbxxa_0, _rbxxa_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : No: () ------------------------------------------- Step 12, which took 0.515418 s (model generation: 0.511595, model checking: 0.003823): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ leq(x_1_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ leq(x_1_0, x_2_0) append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; insert -> [ insert : { _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_3(b) <= True _r_4(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, cons(_byxxa_0, _byxxa_1)) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(a, _fdxxa_1) ; _hfa -> cons(a, cons(_uyxxa_0, _uyxxa_1)) ; h1 -> b ; t1 -> cons(a, _hdxxa_1) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(a, nil) ; h1 -> b ; l2 -> cons(_qexxa_0, _qexxa_1) ; t1 -> cons(b, _rexxa_1) } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, nil) ; _xea -> cons(a, cons(_vxxxa_0, _vxxxa_1)) ; y -> a ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> cons(b, nil) ; _nfa -> cons(b, cons(_nyxxa_0, _nyxxa_1)) ; l -> cons(b, nil) } ------------------------------------------- Step 13, which took 0.759258 s (model generation: 0.751333, model checking: 0.007925): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(a, cons(a, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0) 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_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1), a) <= True _r_1(nil, b) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_4(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_4(x_0_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= True sort(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1), a) <= True _r_1(nil, b) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_4(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_4(x_0_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= True sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> nil ; _hfa -> cons(b, cons(_elzxa_0, _elzxa_1)) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(a, _hcyxa_1) ; h1 -> b ; l2 -> cons(a, _icyxa_1) ; t1 -> nil } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(b, nil) ; y -> b ; z -> cons(_oxyxa_0, _oxyxa_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> nil ; _mfa -> cons(a, nil) ; _nfa -> cons(a, nil) ; l -> cons(a, _ekzxa_1) } ------------------------------------------- Step 14, which took 0.919168 s (model generation: 0.828053, model checking: 0.091115): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(a, cons(a, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None append -> [ append : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_0_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)) <= sort(x_0_1, x_1_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) sort(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> nil ; _hfa -> cons(b, cons(b, _shfya_1)) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(b, _olcya_1) ; l2 -> nil ; t1 -> nil } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, _oscya_1) ; _xea -> cons(b, _pscya_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> nil ; _mfa -> nil ; _nfa -> cons(a, _agfya_1) ; l -> nil } ------------------------------------------- Step 15, which took 1.324863 s (model generation: 1.320173, model checking: 0.004690): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(a, cons(a, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, nil) ; _xea -> cons(b, cons(_higya_0, _higya_1)) ; y -> b ; z -> cons(a, _yxfya_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> a } False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(a, nil) ; _mfa -> cons(b, cons(_nigya_0, _nigya_1)) ; _nfa -> cons(b, nil) ; l -> cons(a, nil) } ------------------------------------------- Step 16, which took 0.963968 s (model generation: 0.956261, model checking: 0.007707): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= True reverse(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_3(a) <= True _r_4(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(a, _wxgya_1) ; _hfa -> cons(b, nil) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, nil) ; _xea -> cons(a, _qthya_1) ; y -> b ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> nil ; _nfa -> nil ; l -> cons(b, nil) } ------------------------------------------- Step 17, which took 4.660216 s (model generation: 0.941039, model checking: 3.719177): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) /\ reverse(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_2_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ insert(x_0_0, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) /\ leq(x_0_0, x_2_0) /\ reverse(x_0_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) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) /\ reverse(x_0_1, x_1_1) /\ reverse(x_0_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) /\ _r_3(x_0_0) /\ _r_4(x_2_0) /\ reverse(x_0_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) /\ _r_4(x_0_0) /\ leq(x_0_0, x_2_0) /\ reverse(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= reverse(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_2_1) /\ reverse(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) /\ leq(x_1_0, x_2_0) /\ reverse(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ reverse(x_1_1, x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ reverse(x_1_1, x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ reverse(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_4(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ reverse(x_1_1, x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ reverse(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_4(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_4(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_4(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> nil ; _mfa -> cons(b, nil) ; _nfa -> cons(a, cons(b, _fspcb_1)) ; l -> nil } ------------------------------------------- Step 18, which took 1.005411 s (model generation: 0.996061, model checking: 0.009350): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_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_4(x_1_0) 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_3(x_1_0) /\ _r_3(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_3(b) <= True _r_4(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_3(b) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(b, nil) ; _hfa -> cons(a, cons(b, _cqrcb_1)) ; h1 -> b ; t1 -> cons(b, nil) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(a, cons(b, _horcb_1)) ; l2 -> cons(b, nil) ; t1 -> cons(_srqcb_0, _srqcb_1) } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : Yes: { _rea -> cons(a, nil) ; x -> b ; y -> a ; z -> cons(_osqcb_0, _osqcb_1) } sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> cons(a, cons(_smrcb_0, _smrcb_1)) ; _nfa -> cons(a, nil) ; l -> cons(a, cons(_smrcb_0, _smrcb_1)) } ------------------------------------------- Step 19, which took 1.934684 s (model generation: 1.921162, model checking: 0.013522): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) 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_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) /\ reverse(x_1_1, x_2_1) append(nil, nil, nil) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) reverse(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(a, _zwrcb_1) ; _hfa -> cons(a, cons(b, _aztcb_1)) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, nil) ; _xea -> cons(a, nil) ; y -> a ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> nil ; _mfa -> cons(a, nil) ; _nfa -> cons(a, nil) ; l -> nil } ------------------------------------------- Step 20, which took 4.356086 s (model generation: 4.331032, model checking: 0.025054): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= 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), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_0_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)) <= sort(x_1_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)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : No: () append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(_wqvcb_0, cons(_boadb_0, _boadb_1)) ; _xea -> cons(a, cons(_ioadb_0, _ioadb_1)) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> nil ; _mfa -> nil ; _nfa -> cons(_unadb_0, cons(_boadb_0, _boadb_1)) ; l -> nil } ------------------------------------------- Step 21, which took 1.777670 s (model generation: 1.771602, model checking: 0.006068): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, nil) <= True _r_3(b) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_1_0, x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_4(x_0_0) /\ reverse(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_0, x_2_1) /\ leq(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= reverse(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_0, x_2_1) /\ leq(x_1_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ leq(x_1_0, x_2_0) append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) reverse(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_1_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_3(b) <= True _r_4(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, nil) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, cons(b, _zybdb_1)) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(a, nil) ; _hfa -> cons(a, cons(b, _vbcdb_1)) ; h1 -> b ; t1 -> cons(a, _nradb_1) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, _xcbdb_1) ; t1 -> nil } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : Yes: { _rea -> cons(a, nil) ; x -> b ; y -> a ; z -> cons(b, _qhbdb_1) } sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> nil ; _xea -> cons(b, cons(b, _occdb_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(a, nil) ; _mfa -> cons(a, cons(a, nil)) ; _nfa -> cons(a, cons(a, nil)) ; l -> cons(a, nil) } ------------------------------------------- Step 22, which took 2.266694 s (model generation: 2.254677, model checking: 0.012017): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(a, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), a) <= True _r_1(cons(x_0_0, x_0_1), b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= 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), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= insert(x_0_0, x_1_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)) <= _r_3(x_1_0) /\ leq(x_1_0, x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ leq(x_1_0, x_2_0) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1), a) <= True _r_1(cons(x_0_0, x_0_1), b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_0_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1), a) <= True _r_1(cons(x_0_0, x_0_1), b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(b, _zicdb_1) ; _hfa -> cons(a, cons(a, _siedb_1)) ; h1 -> a ; t1 -> cons(b, cons(_whedb_0, _whedb_1)) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(b, nil) ; _mfa -> cons(b, cons(_fiedb_0, _fiedb_1)) ; _nfa -> cons(b, cons(_kledb_0, _kledb_1)) ; l -> cons(b, cons(_whedb_0, _whedb_1)) } ------------------------------------------- Step 23, which took 3.269974 s (model generation: 3.248356, model checking: 0.021618): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(a, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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_3(x_1_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) 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_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) reverse(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_3(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(_xledb_0, _xledb_1) ; _hfa -> cons(b, cons(a, _llidb_1)) ; h1 -> a ; t1 -> cons(b, cons(a, _gmidb_1)) } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : Yes: { _bfa -> cons(b, _tcfdb_1) ; h1 -> b ; l2 -> cons(a, _ucfdb_1) ; t1 -> cons(a, _vcfdb_1) } insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, _xgfdb_1) ; _xea -> cons(a, cons(_ilidb_0, _ilidb_1)) ; y -> a ; z -> cons(b, cons(a, _pmidb_1)) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> cons(a, _zkidb_1) ; _mfa -> nil ; _nfa -> nil ; l -> cons(a, cons(a, _mlidb_1)) } ------------------------------------------- Step 24, which took 25.852785 s (model generation: 3.044388, model checking: 22.808397): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, cons(a, nil)), nil) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(a, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= sort(cons(b, cons(a, nil)), cons(a, nil)) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_1) /\ _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_4(x_0_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_1) /\ _r_1(x_1_1, x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) /\ sort(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_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ _r_3(x_2_0) /\ leq(x_0_0, x_1_0) /\ leq(x_0_0, x_2_0) /\ reverse(x_0_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_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0) /\ sort(x_0_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_0_1, x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ reverse(x_0_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_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) /\ leq(x_0_0, x_2_0) /\ reverse(x_0_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_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) /\ leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0) /\ reverse(x_0_1, x_1_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) /\ _r_3(x_2_0) /\ _r_4(x_0_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= leq(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ leq(x_1_0, x_2_0) /\ reverse(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _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_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ reverse(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ reverse(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _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_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; sort -> [ sort : { _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_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ reverse(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(a, cons(a, cons(a, _pbkad_1))) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 25, which took 6.933249 s (model generation: 6.915723, model checking: 0.017526): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, cons(a, nil)), nil) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(a, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= sort(cons(b, cons(a, nil)), cons(a, nil)) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () reverse(nil, nil) <= True : No: () sort(nil, nil) <= True : No: () reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) : Yes: { _gfa -> cons(b, _wclad_1) ; _hfa -> cons(a, _xclad_1) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) : No: () insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) : No: () sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) : Yes: { _wea -> cons(a, nil) ; _xea -> cons(b, cons(_genad_0, _genad_1)) ; y -> a ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) : Yes: { _lfa -> nil ; _mfa -> cons(a, nil) ; _nfa -> cons(a, nil) ; l -> cons(b, cons(_eenad_0, _eenad_1)) } Total time: 59.321461 Learner time: 30.542771 Teacher time: 26.753282 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 reverse(nil, nil) <= True -> 0 sort(nil, nil) <= True -> 0 reverse(cons(h1, t1), _hfa) <= append(_gfa, cons(h1, nil), _hfa) /\ reverse(t1, _gfa) -> 0 append(cons(h1, t1), l2, cons(h1, _bfa)) <= append(t1, l2, _bfa) -> 0 insert(x, cons(y, z), cons(y, _rea)) \/ leq(x, y) <= insert(x, z, _rea) -> 0 sort(cons(y, z), _xea) <= insert(y, _wea, _xea) /\ sort(z, _wea) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_lfa, _nfa) <= reverse(l, _mfa) /\ sort(_mfa, _nfa) /\ sort(l, _lfa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(nil, cons(a, cons(a, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= True append(nil, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True reverse(cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(b, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, nil), cons(a, nil)) reverse(cons(a, cons(b, nil)), cons(b, nil)) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) False <= append(cons(b, nil), cons(b, nil), cons(a, nil)) /\ reverse(nil, cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(b, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) reverse(cons(b, nil), cons(b, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, cons(b, nil))) append(cons(a, nil), nil, cons(a, cons(b, nil))) <= append(nil, nil, cons(b, nil)) sort(cons(a, cons(a, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(b, cons(b, nil), cons(a, nil)) sort(cons(b, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= reverse(cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, cons(a, nil)), nil) /\ sort(cons(a, cons(a, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(a, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= reverse(cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(a, nil)) /\ sort(cons(b, cons(a, nil)), nil) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= reverse(cons(b, nil), cons(a, nil)) False <= reverse(cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, nil), nil) False <= reverse(nil, cons(a, nil)) False <= reverse(nil, cons(b, nil)) /\ sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= sort(cons(b, cons(a, nil)), cons(a, nil)) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(nil, cons(a, cons(a, nil))) False <= sort(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; reverse -> [ reverse : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, nil) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ sort(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ reverse(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ reverse(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _|