Solving ../../benchmarks/smtlib/true/isaplanner_prop51.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, _uxa)) <= butlast(cons(x2, x3), _uxa) } eq_eltlist(_wxa, _xxa) <= butlast(_vxa, _wxa) /\ butlast(_vxa, _xxa) ) (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _yxa)) <= append(t1, l2, _yxa) } eq_eltlist(_bya, _cya) <= append(_zxa, _aya, _bya) /\ append(_zxa, _aya, _cya) ) } properties: { eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) } over-approximation: {append, butlast} 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Solving took 60.396990 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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(b, cons(b, nil))), cons(a, nil), cons(a, cons(b, cons(b, 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, cons(b, nil)), cons(a, nil), cons(b, cons(b, 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, cons(b, cons(a, nil))), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, cons(a, nil)))) append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= append(cons(b, nil), nil, cons(b, nil)) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) 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_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_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True 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_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_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 } ] -- Equality automata are defined for: {elt, eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006256 s (model generation: 0.006193, model checking: 0.000063): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; butlast -> [ butlast : { } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 1, which took 0.006651 s (model generation: 0.006587, model checking: 0.000064): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_micj_0, _micj_1) } butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> nil ; l2 -> nil ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : No: () butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : Yes: { _uxa -> nil } ------------------------------------------- Step 2, which took 0.011252 s (model generation: 0.011167, model checking: 0.000085): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 } 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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(_ricj_0, _ricj_1) ; l2 -> cons(_sicj_0, _sicj_1) ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_uicj_0, _uicj_1) ; _eya -> cons(_vicj_0, _vicj_1) ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 3, which took 0.019397 s (model generation: 0.019294, model checking: 0.000103): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_djcj_0, _djcj_1) ; _eya -> nil ; ys -> cons(_fjcj_0, _fjcj_1) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 4, which took 0.023126 s (model generation: 0.022883, model checking: 0.000243): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 False <= append(cons(a, nil), cons(a, nil), 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)) <= 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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_xjcj_0, cons(_fkcj_0, _fkcj_1)) ; _eya -> nil ; ys -> cons(_zjcj_0, _zjcj_1) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 5, which took 0.031795 s (model generation: 0.031525, model checking: 0.000270): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(cons(a, nil), cons(a, nil)) } Current best model: |_ name: None append -> [ append : { _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)) <= True 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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_vkcj_0, cons(_alcj_0, _alcj_1)) ; _eya -> cons(_wkcj_0, _wkcj_1) ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 6, which took 0.030654 s (model generation: 0.030444, model checking: 0.000210): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 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)) } 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, nil, nil) <= True } ] ; 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 } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_blcj_0, cons(_wlcj_0, _wlcj_1)) } butlast(cons(y, nil), nil) <= True : No: () butlast(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_llcj_0, cons(_jmcj_0, _jmcj_1)) ; _eya -> cons(_mlcj_0, nil) ; ys -> cons(_nlcj_0, cons(_imcj_0, _imcj_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 7, which took 0.037288 s (model generation: 0.037041, model checking: 0.000247): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) 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)) } 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_1(x_0_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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(_lmcj_0, cons(_wncj_0, _wncj_1)) ; l2 -> cons(_mmcj_0, _mmcj_1) ; t1 -> cons(_nmcj_0, nil) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_dncj_0, cons(_cocj_0, _cocj_1)) ; _eya -> cons(b, _encj_1) ; ys -> cons(a, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 8, which took 0.134558 s (model generation: 0.133895, model checking: 0.000663): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True butlast(cons(a, cons(a, nil)), cons(a, nil)) <= True butlast(cons(a, nil), nil) <= True butlast(nil, nil) <= True False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) 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)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), nil) False <= butlast(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_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_0_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_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(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_1, x_1_0) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_gqcj_0, nil) ; _eya -> nil ; ys -> cons(_iqcj_0, cons(_arcj_0, _arcj_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : Yes: { _uxa -> cons(a, _yqcj_1) ; x3 -> cons(_drcj_0, _drcj_1) ; y -> b } ------------------------------------------- Step 9, which took 0.185919 s (model generation: 0.185458, model checking: 0.000461): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, 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)), cons(b, nil)) False <= butlast(cons(a, cons(a, nil)), 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), a) <= 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_3(x_2_1) /\ butlast(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, nil) <= True 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), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= True butlast(nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(cons(x_0_0, x_0_1), a) <= 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_1, x_1_0) butlast(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= True butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(_htcj_0, nil) ; _eya -> cons(_itcj_0, cons(_ytcj_0, _ytcj_1)) ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : Yes: { _uxa -> nil ; x3 -> nil ; y -> b } ------------------------------------------- Step 10, which took 0.184780 s (model generation: 0.184068, model checking: 0.000712): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, 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)), 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)) } 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)) <= 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_2(x_2_1) /\ _r_3(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(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_0, x_1_0) /\ _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(a, cons(_sycj_0, _sycj_1)) ; l2 -> cons(_vucj_0, cons(b, _tycj_1)) ; t1 -> cons(_wucj_0, nil) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_yycj_0, cons(_jxcj_0, _jxcj_1))) ; _eya -> cons(b, _dxcj_1) ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 11, which took 0.428691 s (model generation: 0.427652, model checking: 0.001039): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, 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)) } 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)) <= 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_2(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_0_1) 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) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(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_0, x_1_0) /\ _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_yddj_0, _yddj_1)) ; _eya -> cons(b, cons(_vddj_0, _vddj_1)) ; ys -> cons(_ccdj_0, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 12, which took 0.433674 s (model generation: 0.432475, model checking: 0.001199): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, 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)) } 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_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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_3(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, nil) <= True 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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(_jgdj_0, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_ikdj_0, _ikdj_1)) ; _eya -> cons(b, cons(_akdj_0, _akdj_1)) ; x -> b ; ys -> cons(_vhdj_0, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 13, which took 0.453952 s (model generation: 0.452787, model checking: 0.001165): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), 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)) } 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)) <= 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_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(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_0, x_1_0) /\ _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_vqdj_0, _vqdj_1)) ; _eya -> cons(b, cons(_uqdj_0, _uqdj_1)) ; ys -> cons(b, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 14, which took 0.431864 s (model generation: 0.430154, model checking: 0.001710): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), 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)) } 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_1_0) /\ _r_1(x_1_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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_3(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ butlast(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(b, nil) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_yydj_0, cons(_laej_0, _laej_1))) ; _eya -> cons(b, _qxdj_1) ; x -> b ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 15, which took 0.550135 s (model generation: 0.548823, model checking: 0.001312): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) } 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_0_0, x_2_0) /\ _r_1(x_1_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(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_0, x_1_0) /\ _r_2(x_0_1) butlast(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_1) butlast(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(_ifej_0, nil) ; h1 -> b ; l2 -> cons(a, nil) ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_qiej_0, _qiej_1)) ; _eya -> cons(b, cons(_niej_0, _niej_1)) ; x -> b ; ys -> cons(b, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 16, which took 0.545884 s (model generation: 0.542076, model checking: 0.003808): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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)) <= 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_2(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_0_1) 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) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(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_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_1(x_0_0, x_1_0) /\ _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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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_1(x_0_0, x_1_0) /\ _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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_spej_0, _spej_1)) ; _eya -> cons(b, nil) ; ys -> cons(a, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 17, which took 0.567413 s (model generation: 0.566036, model checking: 0.001377): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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_3(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_ntfj_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 18, which took 0.621311 s (model generation: 0.619826, model checking: 0.001485): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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_3(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, nil) <= True 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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_dfgj_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; ys -> cons(a, _uagj_1) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 19, which took 0.636437 s (model generation: 0.634583, model checking: 0.001854): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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)) <= 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_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(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_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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_tmgj_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; ys -> cons(b, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 20, which took 0.676089 s (model generation: 0.674576, model checking: 0.001513): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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)) <= 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_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True 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_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, cons(x_2_0, x_2_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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(a, _swgj_1) ; l2 -> cons(_twgj_0, cons(b, nil)) ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_aahj_0, cons(_bchj_0, cons(_vzgj_0, _vzgj_1)))) ; _eya -> cons(b, nil) ; x -> b ; ys -> nil } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 21, which took 0.961081 s (model generation: 0.958425, model checking: 0.002656): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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)) <= 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_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_3(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_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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_tohj_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; ys -> cons(a, cons(_tnhj_0, _tnhj_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 22, which took 1.231815 s (model generation: 1.228993, model checking: 0.002822): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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)) <= 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_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_3(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_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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(a, cons(b, cons(_hdij_0, _hdij_1))) ; l2 -> cons(_lshj_0, nil) ; t1 -> cons(b, cons(b, _adij_1)) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_vcij_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; ys -> cons(a, cons(b, _ecij_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 23, which took 2.244388 s (model generation: 2.240910, model checking: 0.003478): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_uqij_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; ys -> cons(b, cons(a, _erij_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 24, which took 2.157554 s (model generation: 2.154618, model checking: 0.002936): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_1_0) /\ _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(b, cons(_ljjj_0, cons(_rjjj_0, _rjjj_1))) ; h1 -> a ; l2 -> cons(b, nil) ; t1 -> cons(b, _kvij_1) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_xkjj_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; x -> b ; ys -> cons(b, cons(a, _wjjj_1)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 25, which took 4.674172 s (model generation: 4.670033, model checking: 0.004139): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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(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_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(nil, nil) <= True } ] ; butlast -> [ butlast : { _r_1(a, a) <= True _r_1(b, 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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_gakj_0, nil)) ; _eya -> cons(a, nil) ; ys -> cons(b, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 26, which took 3.055732 s (model generation: 3.051656, model checking: 0.004076): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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)) <= 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_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_3(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_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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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(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, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : No: () eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(b, cons(_zukj_0, nil)))) ; _eya -> cons(b, cons(b, cons(b, nil))) ; ys -> cons(b, cons(b, cons(a, _zblj_1))) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 27, which took 4.772319 s (model generation: 4.766805, model checking: 0.005514): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_0_1, x_1_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(b, cons(b, cons(_mylj_0, _mylj_1))) ; l2 -> cons(_iklj_0, nil) ; t1 -> cons(b, cons(b, nil)) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(b, cons(_utlj_0, nil)))) ; _eya -> cons(b, cons(b, cons(b, nil))) ; ys -> cons(b, cons(b, nil)) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 28, which took 5.017240 s (model generation: 5.012985, model checking: 0.004255): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(b, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) False <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_1_0) /\ _r_1(x_0_0, x_2_0) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ butlast(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(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_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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) butlast(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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(b, cons(_canj_0, nil)) ; h1 -> b ; l2 -> cons(a, nil) ; t1 -> cons(b, nil) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(b, cons(_rzmj_0, nil))) ; _eya -> cons(b, cons(b, nil)) ; x -> b ; ys -> cons(b, cons(b, cons(_tzmj_0, _tzmj_1))) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 29, which took 4.188167 s (model generation: 4.149253, model checking: 0.038914): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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(b, cons(b, nil))), cons(a, nil), cons(a, cons(b, cons(b, 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, cons(b, nil)), cons(a, nil), cons(b, cons(b, 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, cons(b, cons(a, nil))), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, 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 <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _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_0, x_2_0) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True 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_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_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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(_wtnj_0, cons(_qznj_0, nil)) ; h1 -> a ; l2 -> cons(b, cons(_baoj_0, nil)) ; t1 -> nil } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_iaoj_0, nil)) ; _eya -> cons(b, cons(_cdoj_0, cons(_yznj_0, nil))) ; x -> b ; ys -> cons(_qxnj_0, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 30, which took 5.888342 s (model generation: 5.817144, model checking: 0.071198): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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(b, cons(b, nil))), cons(a, nil), cons(a, cons(b, cons(b, 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, cons(b, nil)), cons(a, nil), cons(b, cons(b, 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, cons(a, nil)))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, cons(b, cons(a, nil))), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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) 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_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True 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 } ] -- 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, _yxa)) <= append(t1, l2, _yxa) : Yes: { _yxa -> cons(b, _rysj_1) ; l2 -> nil ; t1 -> cons(b, nil) } eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_fduj_0, nil)) ; _eya -> cons(b, nil) ; x -> b ; ys -> cons(a, nil) } butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) : No: () ------------------------------------------- Step 31, which took 19.171833 s (model generation: 19.160502, model checking: 0.011331): 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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(b, cons(b, nil))), cons(a, nil), cons(a, cons(b, cons(b, 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, cons(b, nil)), cons(a, nil), cons(b, cons(b, 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, cons(b, cons(a, nil))), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= append(cons(b, nil), nil, cons(b, nil)) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) 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_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_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True 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_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_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 } ] -- 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(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) : Yes: { _dya -> cons(b, cons(_xadk_0, nil)) ; _eya -> cons(b, cons(_pldk_0, cons(_wxck_0, nil))) ; x -> b ; ys -> cons(b, nil) } Total time: 60.396990 Learner time: 59.208867 Teacher time: 0.170903 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, _yxa)) <= append(t1, l2, _yxa) -> 0 eq_eltlist(_eya, ys) <= append(ys, cons(x, nil), _dya) /\ butlast(_dya, _eya) -> 0 butlast(cons(y, cons(x2, x3)), cons(y, _uxa)) <= butlast(cons(x2, x3), _uxa) -> 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(b, cons(b, nil))), cons(a, nil), cons(a, cons(b, cons(b, 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, cons(b, nil)), cons(a, nil), cons(b, cons(b, 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 False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(a, nil)), cons(a, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(b, nil), cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) False <= append(cons(b, cons(b, cons(a, nil))), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, cons(b, cons(a, nil))), cons(b, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, cons(b, nil))), cons(a, nil), cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(b, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) False <= append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, cons(b, cons(a, nil))))) /\ butlast(cons(b, cons(b, cons(b, cons(a, nil)))), cons(b, cons(b, cons(b, nil)))) False <= append(cons(b, nil), cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, cons(b, nil)), cons(b, nil), cons(a, cons(b, cons(a, cons(a, nil))))) <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, cons(a, nil)))) False <= append(cons(b, nil), cons(b, nil), cons(b, cons(a, nil))) /\ butlast(cons(b, cons(a, nil)), cons(b, cons(a, cons(a, nil)))) append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= append(cons(b, nil), nil, cons(b, nil)) append(cons(a, nil), cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= append(nil, cons(a, cons(b, nil)), cons(a, nil)) False <= append(nil, cons(a, nil), cons(a, cons(a, nil))) False <= append(nil, cons(a, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) False <= append(nil, cons(a, nil), cons(b, cons(b, cons(a, nil)))) /\ butlast(cons(b, cons(b, cons(a, nil))), cons(b, cons(b, nil))) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= append(nil, cons(b, cons(a, nil)), cons(a, cons(a, nil))) append(cons(a, nil), cons(b, nil), cons(a, cons(a, nil))) <= append(nil, cons(b, nil), cons(a, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, cons(a, nil))))) /\ butlast(cons(b, cons(a, cons(a, cons(a, nil)))), cons(b, nil)) False <= append(nil, cons(b, nil), cons(b, cons(a, cons(a, nil)))) /\ butlast(cons(b, cons(a, cons(a, nil))), cons(b, nil)) append(cons(a, nil), cons(b, nil), cons(a, cons(b, nil))) <= append(nil, cons(b, nil), cons(b, 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)) False <= butlast(cons(b, cons(a, nil)), cons(a, nil)) False <= butlast(cons(b, cons(a, nil)), cons(b, 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_2(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_0_1) /\ _r_3(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_2_1) /\ _r_3(x_0_1) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _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) 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_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_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True 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_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_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 } ] -- Equality automata are defined for: {elt, eltlist} _|