Solving ../../benchmarks/smtlib/true/isaplanner_prop49.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: { (butlast, F: { butlast(cons(y, nil), nil) <= True butlast(nil, nil) <= True butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) } eq_eltlist(_oo, _po) <= butlast(_no, _oo) /\ butlast(_no, _po) ) (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) } eq_eltlist(_to, _uo) <= append(_ro, _so, _to) /\ append(_ro, _so, _uo) ) (butlastconcat, F: { butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) butlastconcat(x, nil, _vo) <= butlast(x, _vo) } eq_eltlist(_ap, _bp) <= butlastconcat(_yo, _zo, _ap) /\ butlastconcat(_yo, _zo, _bp) ) } properties: { eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) } over-approximation: {append, butlast, butlastconcat} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Solving took 60.971402 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) /\ butlastconcat(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) /\ butlastconcat(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ butlastconcat(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(b, nil)) butlastconcat(cons(b, nil), cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(a, cons(b, cons(a, nil))), cons(a, cons(b, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) butlastconcat(cons(b, nil), cons(a, nil), cons(b, cons(a, cons(a, nil)))) <= append(cons(b, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), nil) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ butlast(x_0_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006150 s (model generation: 0.006063, model checking: 0.000087): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; butlast -> [ butlast : { } ] ; butlastconcat -> [ butlastconcat : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } butlast(cons(y, nil), nil) <= True : Yes: { } butlast(nil, nil) <= True : Yes: { } append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : No: () butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 1, which took 0.006445 s (model generation: 0.006364, model checking: 0.000081): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_rsci_0, _rsci_1) } butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> nil ; l2 -> nil ; t1 -> nil } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> nil ; _xo -> nil ; x -> nil } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : No: () butlastconcat(x, nil, _vo) <= butlast(x, _vo) : Yes: { _vo -> nil ; x -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : Yes: { _mo -> nil } ------------------------------------------- Step 2, which took 0.011031 s (model generation: 0.010942, model checking: 0.000089): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 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 butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_dtci_0, _dtci_1) ; l2 -> cons(_etci_0, _etci_1) ; t1 -> nil } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> nil ; _xo -> cons(_htci_0, _htci_1) ; x -> cons(_itci_0, _itci_1) } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_mtci_0, _mtci_1) ; _dp -> cons(_ntci_0, _ntci_1) ; _ep -> nil ; xs -> nil ; ys -> cons(_qtci_0, _qtci_1) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : Yes: { _vo -> nil ; x -> cons(_utci_0, _utci_1) } butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 3, which took 0.032296 s (model generation: 0.032137, model checking: 0.000159): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 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 butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= butlast(cons(a, 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 } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(_vtci_0, _vtci_1) ; _xo -> cons(_wtci_0, _wtci_1) ; x -> nil ; x2 -> cons(_bvci_0, _bvci_1) } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_suci_0, cons(_bvci_0, _bvci_1)) ; _dp -> cons(_tuci_0, _tuci_1) ; _ep -> nil ; xs -> nil ; ys -> cons(_wuci_0, _wuci_1) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : Yes: { _vo -> cons(_xuci_0, _xuci_1) ; x -> cons(_yuci_0, cons(_bvci_0, _bvci_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 4, which took 0.022725 s (model generation: 0.022494, model checking: 0.000231): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 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 butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= 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)) <= butlast(x_1_1, x_2_1) append(nil, nil, nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_cvci_0, cons(_ixci_0, nil)) } butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_nvci_0, _nvci_1) ; _dp -> nil ; _ep -> cons(_pvci_0, _pvci_1) ; xs -> cons(_qvci_0, _qvci_1) ; ys -> cons(_rvci_0, _rvci_1) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 5, which took 0.025653 s (model generation: 0.025037, model checking: 0.000616): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= butlast(x_1_1, x_2_1) append(nil, nil, nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_yyci_0, _yyci_1) ; _dp -> nil ; _ep -> cons(_azci_0, _azci_1) ; xs -> cons(_bzci_0, _bzci_1) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 6, which took 0.026041 s (model generation: 0.025602, model checking: 0.000439): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= butlast(x_1_1, x_2_1) append(nil, nil, nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= True butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_obdi_0, cons(_fedi_0, _fedi_1)) ; _dp -> nil ; _ep -> cons(_qbdi_0, _qbdi_1) ; xs -> cons(_rbdi_0, _rbdi_1) ; ys -> cons(_sbdi_0, _sbdi_1) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 7, which took 0.046316 s (model generation: 0.045870, model checking: 0.000446): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_1(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_ihdi_0, nil) ; _dp -> nil ; _ep -> cons(_khdi_0, _khdi_1) ; xs -> nil ; ys -> cons(_mhdi_0, cons(_shdi_0, _shdi_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 8, which took 0.047241 s (model generation: 0.046677, model checking: 0.000564): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_1(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_fjdi_0, cons(_kldi_0, _kldi_1)) ; _dp -> cons(_gjdi_0, _gjdi_1) ; _ep -> nil ; xs -> cons(_ijdi_0, _ijdi_1) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 9, which took 0.048292 s (model generation: 0.047684, model checking: 0.000608): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_sldi_0, nil) ; l2 -> nil ; t1 -> cons(_uldi_0, _uldi_1) } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_wodi_0, nil) ; _dp -> nil ; _ep -> cons(_yodi_0, _yodi_1) ; xs -> nil ; ys -> cons(_apdi_0, nil) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 10, which took 0.049890 s (model generation: 0.049225, model checking: 0.000665): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_1(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= True butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_rsdi_0, cons(_wudi_0, _wudi_1)) ; _dp -> cons(_ssdi_0, _ssdi_1) ; _ep -> nil ; xs -> cons(_usdi_0, cons(_vudi_0, _vudi_1)) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 11, which took 0.051182 s (model generation: 0.050430, model checking: 0.000752): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_xxdi_0, nil) ; _dp -> nil ; _ep -> cons(_zxdi_0, _zxdi_1) ; xs -> cons(_aydi_0, cons(_yzdi_0, _yzdi_1)) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 12, which took 0.052797 s (model generation: 0.051747, model checking: 0.001050): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_1(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_1(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_ycei_0, cons(_jhei_0, _jhei_1)) ; _dp -> cons(_zcei_0, nil) ; _ep -> cons(_adei_0, cons(_dhei_0, _dhei_1)) ; xs -> cons(_bdei_0, _bdei_1) ; ys -> cons(_cdei_0, _cdei_1) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 13, which took 0.052846 s (model generation: 0.051828, model checking: 0.001018): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(nil) <= True butlastconcat(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) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> nil ; _xo -> cons(_ljei_0, cons(_loei_0, _loei_1)) ; x -> cons(_mjei_0, cons(_tnei_0, _tnei_1)) ; x2 -> nil } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_zlei_0, cons(_roei_0, _roei_1)) ; _dp -> cons(b, _amei_1) ; _ep -> cons(a, _bmei_1) ; xs -> nil ; ys -> cons(_dmei_0, cons(_qoei_0, _qoei_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 14, which took 0.129392 s (model generation: 0.128177, model checking: 0.001215): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1), a) <= True _r_2(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlastconcat(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) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(a, _pqei_1) ; _xo -> cons(_qqei_0, cons(_qwei_0, _qwei_1)) ; x -> cons(_rqei_0, nil) ; x2 -> cons(_qvei_0, _qvei_1) } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_vuei_0, cons(_uwei_0, _uwei_1)) ; _dp -> cons(a, nil) ; _ep -> cons(_xuei_0, cons(_jwei_0, _jwei_1)) ; xs -> nil ; ys -> cons(_zuei_0, cons(_rwei_0, _rwei_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : Yes: { _mo -> cons(a, _ovei_1) ; x3 -> cons(_tvei_0, _tvei_1) ; y -> b } ------------------------------------------- Step 15, which took 0.196068 s (model generation: 0.193758, model checking: 0.002310): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_2(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_2(nil) <= True _r_3(a) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_3(x_1_0) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_2(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= append(x_0_1, x_1_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_2(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(_xzei_0, cons(_bjfi_0, cons(_hhfi_0, _hhfi_1))) ; _xo -> cons(_yzei_0, nil) ; x -> nil ; x2 -> nil } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_ycfi_0, cons(_bjfi_0, cons(_hhfi_0, _hhfi_1))) ; _dp -> cons(a, _zcfi_1) ; _ep -> nil ; xs -> cons(_bdfi_0, nil) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : Yes: { _vo -> cons(_rgfi_0, cons(_ihfi_0, _ihfi_1)) ; x -> cons(_sgfi_0, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : Yes: { _mo -> nil ; x3 -> nil ; y -> b } ------------------------------------------- Step 16, which took 0.230129 s (model generation: 0.228735, model checking: 0.001394): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlastconcat(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) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(b, cons(_dufi_0, _dufi_1)) ; _xo -> cons(_nofi_0, cons(_vufi_0, _vufi_1)) ; x -> nil ; x2 -> cons(_aufi_0, _aufi_1) ; z -> b } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(b, cons(_xufi_0, _xufi_1)) ; _dp -> cons(b, nil) ; _ep -> cons(_tpfi_0, cons(_nufi_0, _nufi_1)) ; xs -> cons(_upfi_0, _upfi_1) ; ys -> cons(_vpfi_0, cons(_fufi_0, _fufi_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 17, which took 0.253086 s (model generation: 0.251206, model checking: 0.001880): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlastconcat(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) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_owfi_0, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(b, cons(_sdgi_0, _sdgi_1)) ; _xo -> cons(b, cons(_gegi_0, _gegi_1)) ; x -> nil ; x2 -> cons(_vdgi_0, _vdgi_1) ; z -> b } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(b, cons(_ffgi_0, _ffgi_1)) ; _dp -> cons(b, nil) ; _ep -> cons(_vagi_0, cons(_fegi_0, _fegi_1)) ; xs -> cons(_wagi_0, cons(_hegi_0, _hegi_1)) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 18, which took 0.286589 s (model generation: 0.282277, model checking: 0.004312): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1) /\ _r_3(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= append(x_0_1, x_1_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_kfgi_0, cons(_drgi_0, _drgi_1)) ; l2 -> cons(_lfgi_0, nil) ; t1 -> cons(_mfgi_0, nil) } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(b, cons(b, nil)) ; _xo -> cons(_ajgi_0, cons(_prgi_0, _prgi_1)) ; x -> nil ; x2 -> cons(b, cons(_nrgi_0, nil)) ; z -> b } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(b, cons(_urgi_0, _urgi_1)) ; _dp -> cons(b, nil) ; _ep -> nil ; xs -> nil ; ys -> cons(_togi_0, cons(_drgi_0, _drgi_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : Yes: { _vo -> cons(b, cons(b, nil)) ; x -> cons(b, cons(b, cons(_crgi_0, _crgi_1))) } butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 19, which took 0.837383 s (model generation: 0.835160, model checking: 0.002223): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlastconcat(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) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(b, cons(b, nil)) ; _xo -> cons(b, cons(_swhi_0, _swhi_1)) ; x -> nil ; x2 -> cons(b, cons(_qwhi_0, nil)) ; z -> b } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(b, cons(_naii_0, nil)) ; _dp -> cons(b, nil) ; _ep -> cons(a, nil) ; xs -> cons(b, _wqhi_1) ; ys -> cons(_xqhi_0, _xqhi_1) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 20, which took 0.946096 s (model generation: 0.943498, model checking: 0.002598): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= butlast(x_1_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_3(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ butlast(x_1_1, x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= True butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_rcii_0, nil) ; h1 -> b ; l2 -> cons(a, nil) ; t1 -> nil } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(b, cons(a, nil)) ; _xo -> cons(b, cons(b, _ooii_1)) ; x -> nil ; x2 -> cons(a, cons(_lkii_0, nil)) ; z -> b } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(b, cons(_qqii_0, nil)) ; _dp -> cons(b, nil) ; _ep -> cons(a, _weii_1) ; xs -> cons(_xeii_0, _xeii_1) ; ys -> cons(b, cons(_hkii_0, _hkii_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 21, which took 0.863893 s (model generation: 0.861321, model checking: 0.002572): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_3(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_dsii_0, cons(_kcji_0, _kcji_1)) ; l2 -> cons(_esii_0, cons(_mdji_0, nil)) ; t1 -> nil } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> nil ; _xo -> cons(_ltii_0, nil) ; x -> cons(b, nil) ; x2 -> nil ; z -> a } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_xyii_0, nil) ; _dp -> nil ; _ep -> cons(_zyii_0, cons(_ddji_0, _ddji_1)) ; xs -> cons(_azii_0, nil) ; ys -> nil } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 22, which took 1.352393 s (model generation: 1.349308, model checking: 0.003085): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : No: () butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_yrji_0, cons(_ptji_0, cons(_mtji_0, _mtji_1))) ; _dp -> nil ; _ep -> cons(_asji_0, nil) ; xs -> nil ; ys -> cons(_csji_0, cons(_htji_0, _htji_1)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 23, which took 2.168583 s (model generation: 2.115437, model checking: 0.053146): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), nil) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ _r_3(x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ _r_3(x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ butlast(x_0_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ butlast(x_0_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_3(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(_lyji_0, nil) ; l2 -> cons(_myji_0, cons(_teli_0, nil)) ; t1 -> cons(_nyji_0, cons(_ecli_0, nil)) } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> nil ; _xo -> cons(b, cons(_qwli_0, cons(_gali_0, nil))) ; x -> cons(b, nil) ; x2 -> nil } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_ojki_0, nil) ; _dp -> nil ; _ep -> cons(_qjki_0, _qjki_1) ; xs -> cons(_rjki_0, cons(_gali_0, nil)) ; ys -> cons(_sjki_0, cons(_yali_0, nil)) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 24, which took 25.093978 s (model generation: 24.997996, model checking: 0.095982): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) /\ butlastconcat(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) butlastconcat(cons(b, nil), cons(a, nil), cons(b, cons(a, cons(a, nil)))) <= append(cons(b, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), nil) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_1_1) /\ _r_3(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_3(nil) <= True butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ butlast(x_0_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_3(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) : Yes: { _qo -> cons(b, _ndqi_1) ; l2 -> cons(_odqi_0, cons(_lrri_0, nil)) ; t1 -> cons(b, nil) } butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) : Yes: { _wo -> cons(_qmqi_0, cons(b, nil)) ; _xo -> cons(b, cons(_hlri_0, nil)) ; x -> cons(b, nil) ; x2 -> cons(b, cons(_grti_0, nil)) } eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_hvqi_0, nil) ; _dp -> nil ; _ep -> cons(b, nil) ; xs -> cons(b, cons(_ljri_0, nil)) ; ys -> cons(_lvqi_0, nil) } butlastconcat(x, nil, _vo) <= butlast(x, _vo) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) : No: () ------------------------------------------- Step 25, which took 27.116682 s (model generation: 27.108601, model checking: 0.008081): Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) /\ butlastconcat(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ butlastconcat(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(b, nil)) butlastconcat(cons(b, nil), cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(a, cons(b, cons(a, nil))), cons(a, cons(b, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) butlastconcat(cons(b, nil), cons(a, nil), cons(b, cons(a, cons(a, nil)))) <= append(cons(b, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), nil) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ butlast(x_0_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) : Yes: { _cp -> cons(_ztbj_0, nil) ; _dp -> nil ; _ep -> cons(_bubj_0, cons(_lhcj_0, nil)) ; xs -> cons(_cubj_0, cons(_ggcj_0, nil)) ; ys -> cons(_dubj_0, cons(_lhcj_0, nil)) } Total time: 60.971402 Learner time: 59.767574 Teacher time: 0.185602 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 butlast(cons(y, nil), nil) <= True -> 0 butlast(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _qo)) <= append(t1, l2, _qo) -> 0 butlastconcat(x, cons(z, x2), _xo) <= append(x, _wo, _xo) /\ butlast(cons(z, x2), _wo) -> 0 eq_eltlist(_dp, _ep) <= append(xs, ys, _cp) /\ butlast(_cp, _dp) /\ butlastconcat(xs, ys, _ep) -> 0 butlastconcat(x, nil, _vo) <= butlast(x, _vo) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _mo)) <= butlast(cons(x2, x3), _mo) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(cons(b, cons(a, cons(a, nil))), cons(b, cons(a, nil))) <= True butlast(cons(b, cons(a, nil)), cons(b, nil)) <= True butlast(nil, nil) <= True butlastconcat(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, cons(a, nil)), nil, cons(a, nil)) <= True butlastconcat(cons(a, nil), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True butlastconcat(cons(a, nil), cons(a, nil), cons(a, nil)) <= True butlastconcat(cons(a, nil), nil, nil) <= True butlastconcat(nil, cons(a, cons(a, nil)), cons(a, nil)) <= True butlastconcat(nil, cons(a, nil), nil) <= True butlastconcat(nil, nil, nil) <= True append(cons(a, cons(a, cons(a, nil))), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) /\ butlastconcat(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) /\ butlastconcat(cons(a, cons(a, nil)), cons(a, cons(a, nil)), cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(a, nil)) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(a, nil))) /\ butlastconcat(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(cons(a, nil), cons(b, cons(a, nil)), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(a, nil)) /\ butlastconcat(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(b, nil)) butlastconcat(cons(b, nil), cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(a, cons(b, cons(a, nil))), cons(a, cons(b, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) butlastconcat(cons(b, nil), cons(a, nil), cons(b, cons(a, cons(a, nil)))) <= append(cons(b, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ butlast(cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= append(nil, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) /\ butlast(cons(a, cons(a, cons(a, nil))), nil) False <= append(nil, cons(a, cons(a, nil)), cons(a, nil)) False <= append(nil, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ butlastconcat(nil, cons(a, cons(a, nil)), nil) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) butlastconcat(nil, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= append(nil, cons(b, cons(a, nil)), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) butlastconcat(nil, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= append(nil, cons(b, cons(b, nil)), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, cons(a, nil))) False <= butlast(cons(a, nil), cons(a, nil)) butlastconcat(cons(b, cons(b, cons(a, nil))), nil, cons(b, cons(b, nil))) <= butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= butlastconcat(cons(a, cons(a, nil)), nil, nil) False <= butlastconcat(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, cons(a, nil))) False <= butlastconcat(cons(a, nil), nil, cons(a, nil)) False <= butlastconcat(cons(b, nil), cons(a, nil), cons(a, nil)) False <= butlastconcat(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= butlastconcat(nil, cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_0) /\ _r_1(x_0_0, x_2_0) /\ _r_3(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True } ] ; butlastconcat -> [ butlastconcat : { _r_1(a, a) <= True _r_1(b, b) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_3(x_0_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ butlast(x_0_1, x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, nil) <= True butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_2(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) butlastconcat(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ butlast(x_0_1, x_2_1) butlastconcat(cons(x_0_0, x_0_1), nil, nil) <= _r_2(x_0_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_2_1) butlastconcat(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_1) butlastconcat(nil, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) butlastconcat(nil, nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _|