Solving ../../benchmarks/smtlib/true/mem_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: { (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) } eq_eltlist(_oba, _pba) <= append(_mba, _nba, _oba) /\ append(_mba, _nba, _pba) ) (reverse, F: { reverse(nil, nil) <= True reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) } eq_eltlist(_tba, _uba) <= reverse(_sba, _tba) /\ reverse(_sba, _uba) ) (mem, P: { mem(h, cons(h, t)) <= True eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) False <= mem(e, nil) } ) } properties: { mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) } over-approximation: {append, reverse} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 0 } Solving took 60.388374 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= 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 False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(b, nil)) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= append(cons(b, nil), cons(b, nil), cons(a, 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))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(b, nil)))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, cons(b, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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) /\ mem(x_1_0, 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_4(x_0_0) /\ _r_4(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006510 s (model generation: 0.006252, model checking: 0.000258): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; mem -> [ mem : { } ] ; reverse -> [ reverse : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } mem(h, cons(h, t)) <= True : Yes: { h -> b } reverse(nil, nil) <= True : Yes: { } reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : No: () append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 1, which took 0.006300 s (model generation: 0.006233, model checking: 0.000067): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True mem(b, cons(b, nil)) <= True reverse(nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; mem -> [ mem : { mem(b, cons(x_1_0, x_1_1)) <= True } ] ; reverse -> [ reverse : { reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_tsxs_0, _tsxs_1) } mem(h, cons(h, t)) <= True : Yes: { h -> a } reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : No: () append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> nil ; l2 -> nil ; t1 -> nil } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> b ; h -> a ; t -> nil } False <= mem(e, nil) : No: () ------------------------------------------- Step 2, which took 0.008375 s (model generation: 0.008278, model checking: 0.000097): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(b, cons(b, nil)) <= True reverse(nil, nil) <= True mem(b, nil) <= mem(b, 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 } ] ; mem -> [ mem : { mem(a, cons(x_1_0, x_1_1)) <= True mem(b, cons(x_1_0, x_1_1)) <= True mem(b, nil) <= True } ] ; reverse -> [ reverse : { reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(_ctxs_0, _ctxs_1) ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(_etxs_0, _etxs_1) ; l2 -> cons(_ftxs_0, _ftxs_1) ; t1 -> nil } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> a ; h -> b ; t -> nil } False <= mem(e, nil) : Yes: { e -> b } ------------------------------------------- Step 3, which took 0.023573 s (model generation: 0.023441, model checking: 0.000132): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True mem(a, nil) <= mem(a, cons(b, nil)) False <= mem(b, cons(a, nil)) False <= mem(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 } ] ; mem -> [ mem : { _r_1(b) <= True mem(a, cons(x_1_0, x_1_1)) <= True mem(a, nil) <= True mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_0) } ] ; reverse -> [ reverse : { reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : No: () append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(a, _mtxs_1) ; e -> b ; l1 -> cons(b, _otxs_1) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> b ; h -> a ; t -> cons(b, _rtxs_1) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : Yes: { e -> a } ------------------------------------------- Step 4, which took 0.052437 s (model generation: 0.052094, model checking: 0.000343): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(b, nil), cons(a, 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 } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(a) <= True _r_3(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; 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 } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(_huxs_0, _huxs_1) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(a, nil) ; e -> b ; l1 -> cons(a, cons(_vvxs_0, _vvxs_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> a ; h -> b ; t -> cons(a, _uuxs_1) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> b ; h -> a ; t -> cons(a, nil) } False <= mem(e, nil) : No: () ------------------------------------------- Step 5, which took 0.086268 s (model generation: 0.085807, model checking: 0.000461): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(nil, nil) <= True False <= append(nil, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _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), 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_4(x_1_0) append(nil, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= True _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_4(a) <= True reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, _cwxs_1) } mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(_fwxs_0, _fwxs_1) ; _rba -> cons(_gwxs_0, _gwxs_1) ; h1 -> b ; t1 -> cons(a, _hwxs_1) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(b, nil) ; e -> a ; l1 -> cons(a, cons(_oyxs_0, _oyxs_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> b ; h -> a ; t -> cons(a, cons(b, _syxs_1)) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> a ; h -> b ; t -> cons(b, nil) } False <= mem(e, nil) : No: () ------------------------------------------- Step 6, which took 0.131936 s (model generation: 0.131249, model checking: 0.000687): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(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(b, nil), cons(a, nil)) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(b, 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)) <= _r_3(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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(nil, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; 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) /\ _r_3(x_1_0) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(b, _qzxs_1) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(b, _bays_1) ; l2 -> cons(b, _cays_1) ; t1 -> nil } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(a, nil) ; e -> b ; l1 -> cons(a, cons(b, _fcys_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> a ; h -> b ; t -> cons(b, cons(a, _ncys_1)) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 7, which took 0.238708 s (model generation: 0.237142, model checking: 0.001566): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(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(b, nil), cons(a, nil)) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _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), 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_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) append(nil, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_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_2(x_0_1) /\ _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _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) /\ reverse(x_0_1, x_1_1) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(b, cons(_tmys_0, _tmys_1)) ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(a, nil) ; e -> b ; l1 -> cons(b, cons(a, _zkys_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 8, which took 0.241078 s (model generation: 0.239772, model checking: 0.001306): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(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, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(b, nil), cons(a, nil)) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_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)) <= mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) append(nil, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; 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_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) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(b, nil) ; _rba -> cons(a, cons(b, _kuys_1)) ; h1 -> b ; t1 -> cons(_zmys_0, nil) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(b, nil) ; l2 -> cons(a, _mpys_1) ; t1 -> nil } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(b, nil) ; e -> a ; l1 -> cons(a, nil) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 9, which took 0.303869 s (model generation: 0.302253, model checking: 0.001616): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(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, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _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)) <= mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; 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(x_0_1, x_1_1) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(b, _zvys_1) ; _rba -> cons(a, cons(b, _vdzs_1)) ; h1 -> b ; t1 -> cons(b, _bwys_1) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(b, nil) ; e -> a ; l1 -> cons(b, cons(a, _kbzs_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 10, which took 0.355274 s (model generation: 0.353487, model checking: 0.001787): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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 mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= append(nil, cons(b, nil), cons(a, nil)) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_3(a) <= True _r_4(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(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(x_0_1, x_1_1) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(b, cons(_onzs_0, _onzs_1)) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(a, _cjzs_1) ; h1 -> b ; l2 -> cons(a, _djzs_1) ; t1 -> nil } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 11, which took 0.439020 s (model generation: 0.436747, model checking: 0.002273): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, 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, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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_2(x_2_1) /\ _r_3(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_3(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) append(nil, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_3(a) <= True _r_4(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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(a, _rrzs_1) ; _rba -> cons(b, cons(b, _xaat_1)) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(_rxzs_0, cons(b, _xaat_1)) ; h1 -> b ; l2 -> cons(b, _sxzs_1) ; t1 -> cons(a, _txzs_1) } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 12, which took 0.741769 s (model generation: 0.738749, model checking: 0.003020): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, 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, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_3(a) <= True _r_4(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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(a, _ggat_1) ; _rba -> cons(b, cons(a, _ssat_1)) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 13, which took 0.769592 s (model generation: 0.766406, model checking: 0.003186): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) reverse(cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(b, nil), cons(a, cons(b, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, 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, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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) /\ _r_3(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= 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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_3(a) <= True _r_4(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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(b, _bbbt_1) ; _rba -> cons(b, _cbbt_1) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(b, nil) ; h1 -> a ; l2 -> cons(a, _afbt_1) ; t1 -> cons(b, _bfbt_1) } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 14, which took 0.960901 s (model generation: 0.957392, model checking: 0.003509): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, 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, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _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_3(x_0_0) /\ _r_3(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; 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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(a, _rrbt_1) ; _rba -> cons(a, cons(b, _ject_1)) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 15, which took 1.054839 s (model generation: 1.051513, model checking: 0.003326): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, 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, cons(a, nil))) <= append(nil, cons(b, nil), cons(b, cons(a, nil))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1(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_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_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_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) append(nil, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_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_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(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(x_0_1, x_1_1) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(b, nil) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(a, cons(a, nil)) ; e -> b ; l1 -> cons(b, _zuct_1) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 16, which took 1.074381 s (model generation: 0.960487, model checking: 0.113894): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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)) <= mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : No: () append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(a, cons(a, nil)) ; e -> b ; l1 -> cons(a, cons(b, _zjdt_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 17, which took 1.100377 s (model generation: 1.026314, model checking: 0.074063): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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)) <= mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(_pedu_0, cons(a, cons(b, _itdu_1))) ; _rba -> cons(b, cons(b, nil)) ; h1 -> b ; t1 -> cons(a, cons(b, nil)) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 18, which took 1.485797 s (model generation: 1.480980, model checking: 0.004817): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(b, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_3(x_0_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(b, _juou_1) ; _rba -> cons(b, cons(a, nil)) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(b, cons(b, nil)) ; e -> a ; l1 -> cons(a, _udpu_1) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 19, which took 1.448789 s (model generation: 1.441883, model checking: 0.006906): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, cons(a, nil)) reverse(cons(b, cons(a, nil)), cons(a, nil)) <= append(cons(a, nil), cons(b, nil), cons(a, nil)) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_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) /\ _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_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_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) append(nil, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_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_1_1) /\ _r_3(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(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, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(b, cons(a, _plqu_1)) ; _rba -> cons(a, nil) ; h1 -> a ; t1 -> cons(_rzpu_0, _rzpu_1) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 20, which took 1.491770 s (model generation: 1.485071, model checking: 0.006699): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _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_3(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_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_2(x_1_1) /\ _r_3(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(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, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(a, cons(_qnru_0, _qnru_1)) ; h1 -> a ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 21, which took 1.879118 s (model generation: 1.849751, model checking: 0.029367): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_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)) <= mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(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(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(_szru_0, cons(_zjxu_0, cons(b, _hzsu_1))) ; _rba -> cons(a, cons(a, nil)) ; h1 -> a ; t1 -> cons(b, _uzru_1) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : Yes: { _vba -> cons(b, cons(b, nil)) ; e -> a ; l1 -> cons(b, cons(a, _kssu_1)) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 22, which took 1.565358 s (model generation: 1.562521, model checking: 0.002837): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True reverse(cons(a, nil), cons(a, nil)) <= True reverse(cons(b, nil), cons(b, nil)) <= True reverse(nil, nil) <= True False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1(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_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_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) /\ 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) /\ 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_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(x_0_1, x_1_1) reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; 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(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(x_0_1, x_1_1) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(a, nil) ; _rba -> cons(a, cons(b, _xayu_1)) ; h1 -> b ; t1 -> cons(a, nil) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : No: () mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 23, which took 3.894804 s (model generation: 3.885797, model checking: 0.009007): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= 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 False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _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_3(x_0_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ mem(x_1_0, x_2_1) /\ reverse(x_0_1, x_1_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 mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, 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_1_1) /\ _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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_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_1_1) /\ _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(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(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> nil ; _rba -> cons(b, cons(b, _aizu_1)) ; h1 -> b ; t1 -> nil } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(b, _sazu_1) ; h1 -> a ; l2 -> cons(b, cons(b, _vgzu_1)) ; t1 -> nil } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 24, which took 7.361218 s (model generation: 7.355367, model checking: 0.005851): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= 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 False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(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))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, cons(b, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _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_4(x_0_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= mem(x_1_0, x_2_1) /\ reverse(x_0_1, x_1_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) /\ 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) /\ reverse(x_1_1, x_2_1) append(nil, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_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_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(x_0_1, x_1_1) reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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_1_1) /\ _r_3(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(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, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) : Yes: { _qba -> cons(a, nil) ; _rba -> cons(b, cons(a, _glav_1)) ; h1 -> a ; t1 -> cons(a, nil) } append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(_uaav_0, cons(b, _zgav_1)) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> cons(b, _waav_1) } mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 25, which took 12.501610 s (model generation: 12.188750, model checking: 0.312860): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= 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 False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(b, nil)) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= append(cons(b, nil), cons(b, nil), cons(a, 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))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, cons(b, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _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)) <= mem(x_1_0, x_2_1) /\ reverse(x_0_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 mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(a, cons(a, nil)) ; l2 -> cons(a, _blbv_1) ; t1 -> cons(b, nil) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () ------------------------------------------- Step 26, which took 20.147479 s (model generation: 20.129829, model checking: 0.017650): Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= 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 False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(b, nil)) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= append(cons(b, nil), cons(b, nil), cons(a, 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))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, cons(b, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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) /\ mem(x_1_0, 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_4(x_0_0) /\ _r_4(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () mem(h, cons(h, t)) <= True : No: () reverse(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) : Yes: { _lba -> cons(b, cons(b, _sxdy_1)) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> cons(b, _yqdy_1) } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () False <= mem(e, nil) : No: () Total time: 60.388374 Learner time: 58.763566 Teacher time: 0.607585 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 reverse(nil, nil) <= True -> 0 reverse(cons(h1, t1), _rba) <= append(_qba, cons(h1, nil), _rba) /\ reverse(t1, _qba) -> 0 append(cons(h1, t1), l2, cons(h1, _lba)) <= append(t1, l2, _lba) -> 0 mem(e, _vba) <= mem(e, l1) /\ reverse(l1, _vba) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 False <= mem(e, nil) -> 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, cons(a, nil)), cons(b, nil), cons(b, cons(a, cons(b, 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, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= 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 False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) /\ reverse(cons(b, nil), cons(a, cons(a, cons(b, nil)))) reverse(cons(b, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= append(cons(a, cons(a, cons(b, nil))), cons(b, nil), cons(b, cons(b, nil))) /\ reverse(cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) reverse(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ reverse(nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) /\ reverse(nil, 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(a, nil)), cons(a, nil)) <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ reverse(cons(a, nil), cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(b, nil)) /\ reverse(nil, cons(b, nil)) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(a, cons(b, nil)))) <= append(cons(b, nil), cons(b, nil), cons(a, 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))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(b, nil)))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) reverse(cons(a, nil), cons(a, cons(a, nil))) <= append(nil, cons(a, nil), cons(a, cons(a, nil))) reverse(cons(a, nil), cons(b, cons(a, nil))) <= append(nil, cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(b, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, cons(b, 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))) False <= mem(a, cons(a, cons(a, nil))) /\ reverse(cons(a, cons(a, nil)), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, cons(b, cons(a, nil))) /\ reverse(cons(b, cons(a, nil)), cons(a, nil)) False <= mem(b, nil) False <= reverse(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= reverse(cons(a, cons(b, nil)), cons(a, nil)) False <= reverse(cons(a, nil), cons(b, cons(b, nil))) False <= reverse(cons(a, nil), cons(b, nil)) False <= reverse(cons(b, cons(a, nil)), cons(b, cons(b, nil))) False <= reverse(cons(b, cons(a, nil)), cons(b, nil)) False <= reverse(cons(b, nil), cons(a, cons(a, nil))) False <= reverse(cons(b, nil), cons(a, nil)) reverse(cons(b, nil), cons(a, cons(b, nil))) <= reverse(nil, cons(a, nil)) reverse(cons(a, nil), cons(b, cons(a, nil))) <= reverse(nil, cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _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) /\ mem(x_1_0, 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_4(x_0_0) /\ _r_4(x_2_0) /\ mem(x_1_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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 mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; reverse -> [ reverse : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) /\ mem(x_0_0, 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(x_0_1, x_1_1) reverse(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= mem(x_0_0, x_1_1) /\ reverse(x_0_1, x_1_1) reverse(nil, cons(x_1_0, x_1_1)) <= True reverse(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _|