Solving ../../benchmarks/smtlib/true/sort_append.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} ; nat -> {s, z} } definition: { (leq, P: { leq(a, y) <= True leq(b, b) <= True False <= leq(b, a) } ) (insert, F: { insert(x, nil, cons(x, nil)) <= True insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) } eq_eltlist(_br, _cr) <= insert(_zq, _ar, _br) /\ insert(_zq, _ar, _cr) ) (sort, F: { sort(nil, nil) <= True sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) } eq_eltlist(_gr, _hr) <= sort(_fr, _gr) /\ sort(_fr, _hr) ) (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) } eq_eltlist(_lr, _mr) <= append(_jr, _kr, _lr) /\ append(_jr, _kr, _mr) ) } properties: { eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) } over-approximation: {append, insert, sort} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Solving took 60.054064 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, cons(b, nil))), cons(a, cons(a, cons(b, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, cons(a, nil))), cons(a, cons(b, cons(a, cons(a, nil))))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True append(cons(a, cons(a, cons(a, cons(a, nil)))), nil, cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(b, cons(a, nil)))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(b, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_0, x_2_1) /\ _r_3(x_0_1) /\ insert(x_0_0, x_1_1, x_2_1) /\ sort(x_0_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_1_1) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_0_1, x_1_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_0_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_1_1, 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_1) /\ _r_2(x_0_1) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, 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_1) /\ _r_3(x_0_1) /\ _r_3(x_2_1) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.009140 s (model generation: 0.008959, model checking: 0.000181): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; insert -> [ insert : { } ] ; leq -> [ leq : { } ] ; sort -> [ sort : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } insert(x, nil, cons(x, nil)) <= True : Yes: { x -> b } leq(a, y) <= True : Yes: { y -> b } leq(b, b) <= True : Yes: { } sort(nil, nil) <= True : Yes: { } append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : No: () eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : No: () insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 1, which took 0.016255 s (model generation: 0.016065, model checking: 0.000190): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True insert(b, nil, cons(b, nil)) <= True leq(a, b) <= True leq(b, b) <= True sort(nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; insert -> [ insert : { insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_owjca_0, _owjca_1) } insert(x, nil, cons(x, nil)) <= True : Yes: { x -> a } leq(a, y) <= True : Yes: { y -> a } leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> nil ; l2 -> nil ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : No: () insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : Yes: { _yq -> cons(_uwjca_0, _uwjca_1) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(_zwjca_0, _zwjca_1) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> b ; y -> b } False <= leq(b, a) : No: () ------------------------------------------- Step 2, which took 0.014861 s (model generation: 0.014724, model checking: 0.000137): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) \/ leq(b, a) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, a) <= True leq(b, b) <= True } ] ; sort -> [ sort : { sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(_gxjca_0, _gxjca_1) ; l2 -> cons(_hxjca_0, _hxjca_1) ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(b, _jxjca_1) ; _or -> nil ; _pr -> cons(a, _lxjca_1) ; l -> nil } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> b } False <= leq(b, a) : Yes: { } ------------------------------------------- Step 3, which took 0.027765 s (model generation: 0.027577, model checking: 0.000188): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(nil, nil) <= True insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : No: () eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, nil) ; _or -> nil ; _pr -> cons(_nyjca_0, cons(_nzjca_0, _nzjca_1)) ; l -> nil } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(b, _uyjca_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 4, which took 0.024130 s (model generation: 0.023863, model checking: 0.000267): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(nil, nil) <= True False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) /\ sort(cons(a, nil), cons(a, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(b, nil) ; l2 -> nil ; t1 -> cons(_szjca_0, nil) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, nil) ; _or -> cons(a, _bakca_1) ; _pr -> cons(_cakca_0, cons(_pbkca_0, _pbkca_1)) ; l -> cons(_dakca_0, _dakca_1) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(b, _zakca_1) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 5, which took 0.055254 s (model generation: 0.055027, model checking: 0.000227): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) /\ sort(cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), nil, cons(a, cons(b, nil))) <= append(cons(a, nil), nil, cons(b, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : No: () eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : No: () insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(_jckca_0, _jckca_1) ; _er -> cons(_kckca_0, _kckca_1) ; y -> a ; z -> cons(b, _mckca_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 6, which took 0.064138 s (model generation: 0.063795, model checking: 0.000343): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) /\ sort(cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), nil, cons(a, cons(b, nil))) <= append(cons(a, nil), nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(b) <= True _r_2(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_2(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0) /\ leq(x_0_0, x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(b) <= True _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0) /\ leq(x_0_0, x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : No: () insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(a, _tekca_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 7, which took 0.068406 s (model generation: 0.065913, model checking: 0.002493): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 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(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, cons(a, nil)), nil, cons(a, cons(b, nil))) <= append(cons(a, nil), nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a) <= True _r_2(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= leq(x_0_0, x_1_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0) /\ _r_2(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a) <= True _r_2(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0) /\ _r_1(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_2(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a) <= True _r_2(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(_sikca_0, _sikca_1) ; h1 -> b ; l2 -> cons(a, _tikca_1) ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(b, nil)) ; _or -> cons(b, nil) ; _pr -> cons(b, _skkca_1) ; l -> cons(b, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(a, cons(_zzkca_0, _zzkca_1)) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> a } False <= leq(b, a) : No: () ------------------------------------------- Step 8, which took 0.094476 s (model generation: 0.093160, model checking: 0.001316): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 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(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, cons(a, nil)), nil, cons(a, cons(b, nil))) <= append(cons(a, nil), nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, nil))) <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : No: () eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(b, cons(_lhlca_0, _lhlca_1)) ; _or -> cons(_qclca_0, nil) ; _pr -> cons(a, cons(_bhlca_0, _bhlca_1)) ; l -> cons(b, _sclca_1) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(b, nil) ; _er -> cons(b, nil) ; y -> a ; z -> cons(b, _eflca_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 9, which took 0.198059 s (model generation: 0.196565, model checking: 0.001494): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 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(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, cons(a, nil)), nil, cons(a, cons(b, nil))) <= append(cons(a, nil), nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) sort(cons(a, nil), cons(a, cons(a, nil))) <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), a) <= _r_2(x_0_0) _r_1(nil, a) <= True _r_1(nil, b) <= True _r_2(b) <= True _r_3(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_0) /\ _r_2(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1), a) <= _r_2(x_0_0) _r_1(nil, a) <= True _r_1(nil, b) <= True _r_2(b) <= True _r_3(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_2(x_0_0) /\ _r_2(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_0) /\ _r_3(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, _zjlca_1) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(b, _qklca_1) ; h1 -> a ; l2 -> nil ; t1 -> cons(b, cons(_nulca_0, _nulca_1)) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(_ztlca_0, _ztlca_1)) ; _or -> nil ; _pr -> cons(a, nil) ; l -> nil } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(a, _jqlca_1) ; _er -> cons(b, _kqlca_1) ; y -> b ; z -> cons(_mqlca_0, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 10, which took 0.242905 s (model generation: 0.241091, model checking: 0.001814): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 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(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) append(cons(a, cons(a, nil)), nil, cons(a, cons(b, nil))) <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_0) _r_1(nil) <= True _r_2(b) <= True _r_3(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ insert(x_0_0, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) } ] ; insert -> [ insert : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_0) _r_1(nil) <= True _r_2(b) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_0) _r_1(nil) <= True _r_2(b) <= True _r_3(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_evlca_0, cons(a, _mcmca_1)) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(a, nil) ; l2 -> nil ; t1 -> cons(a, _zvlca_1) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, nil) ; _or -> nil ; _pr -> cons(b, nil) ; l -> nil } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : Yes: { _yq -> cons(_ezlca_0, _ezlca_1) ; x -> b ; y -> a ; z -> cons(a, nil) } sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(a, nil) ; _er -> cons(a, cons(a, _zcmca_1)) ; y -> a ; z -> cons(_tzlca_0, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> b ; y -> b ; z -> cons(a, _rcmca_1) } False <= leq(b, a) : No: () ------------------------------------------- Step 11, which took 0.334303 s (model generation: 0.332777, model checking: 0.001526): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, nil)) <= insert(a, cons(a, nil), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_2(a) <= True _r_3(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) sort(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(nil) <= True _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_2(a) <= True _r_3(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) sort(cons(x_0_0, x_0_1), nil) <= _r_3(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(_afmca_0, _afmca_1) ; l2 -> cons(b, _bfmca_1) ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, nil) ; _or -> cons(a, nil) ; _pr -> cons(b, _lfmca_1) ; l -> cons(b, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(a, nil) ; _er -> cons(a, nil) ; y -> a ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 12, which took 0.372917 s (model generation: 0.329383, model checking: 0.043534): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), 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 <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, nil) <= True _r_2(nil) <= True _r_3(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0) /\ sort(x_0_1, x_1_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= leq(x_1_0, x_2_0) append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, nil) <= True _r_2(nil) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_1_1) /\ _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, nil) <= True _r_2(nil) <= True _r_3(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(b, _csmca_1) ; l2 -> cons(b, cons(_jvsca_0, _jvsca_1)) ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(b, nil)) ; _or -> cons(a, nil) ; _pr -> cons(b, cons(_uusca_0, nil)) ; l -> cons(b, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(a, nil) ; _er -> cons(a, cons(_vusca_0, cons(_wusca_0, _wusca_1))) ; y -> b ; z -> cons(b, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> b ; z -> cons(_yusca_0, _yusca_1) } False <= leq(b, a) : No: () ------------------------------------------- Step 13, which took 1.042905 s (model generation: 1.039854, model checking: 0.003051): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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 <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(nil) <= True _r_3(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, 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_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(nil) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(nil) <= True _r_3(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(b, cons(_tktca_0, nil)) ; h1 -> b ; l2 -> nil ; t1 -> cons(b, cons(b, _uktca_1)) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(_zvtca_0, nil)) ; _or -> cons(a, cons(a, nil)) ; _pr -> cons(a, nil) ; l -> cons(b, cons(_bwtca_0, nil)) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : Yes: { _yq -> cons(_ketca_0, cons(_sitca_0, _sitca_1)) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(b, cons(_titca_0, _titca_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> a ; z -> cons(_sitca_0, _sitca_1) } False <= leq(b, a) : No: () ------------------------------------------- Step 14, which took 2.261958 s (model generation: 2.259459, model checking: 0.002499): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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 <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_2(a, a) <= True _r_2(b, a) <= True _r_2(b, b) <= True _r_3(nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_2(x_0_0, x_1_0) /\ _r_2(x_0_0, x_2_0) /\ append(x_0_1, x_1_1, x_2_1) /\ insert(x_0_0, x_1_1, x_2_1) /\ sort(x_0_1, x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_2(x_0_0, x_2_0) /\ 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)) <= _r_2(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_3(nil) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_2(a, a) <= True _r_2(b, a) <= True _r_2(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(_iduca_0, _iduca_1) ; l2 -> nil ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(b, nil)) ; _or -> cons(a, nil) ; _pr -> cons(a, cons(a, nil)) ; l -> cons(b, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(b, nil) ; _er -> cons(b, cons(_nkuca_0, nil)) ; y -> a ; z -> cons(b, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 15, which took 2.114125 s (model generation: 2.107022, model checking: 0.007103): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, 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_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; insert -> [ insert : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(b, _wnuca_1) ; l2 -> cons(a, _xnuca_1) ; t1 -> nil } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, nil) ; _or -> nil ; _pr -> cons(b, cons(a, cons(_vcwca_0, _vcwca_1))) ; l -> nil } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(a, nil) ; _er -> cons(b, cons(_mawca_0, nil)) ; y -> b ; z -> cons(b, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 16, which took 2.900889 s (model generation: 2.897690, model checking: 0.003199): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(nil) <= True _r_3(b) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_4(a) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(a, nil) ; l2 -> nil ; t1 -> cons(b, nil) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(a, nil)) ; _or -> cons(a, nil) ; _pr -> cons(b, cons(_fpwca_0, _fpwca_1)) ; l -> cons(a, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(a, nil) ; _er -> cons(a, cons(_hwwca_0, _hwwca_1)) ; y -> b ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 17, which took 3.018960 s (model generation: 3.001994, model checking: 0.016966): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, 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, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) 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) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_jwwca_0, cons(b, cons(b, _ggzca_1))) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(_mwwca_0, nil) ; h1 -> a ; l2 -> cons(_nwwca_0, cons(_hgzca_0, _hgzca_1)) ; t1 -> cons(b, _owwca_1) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(a, cons(a, nil)) ; _or -> cons(_yhxca_0, nil) ; _pr -> cons(a, nil) ; l -> cons(b, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : Yes: { _yq -> cons(b, _fmxca_1) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> nil ; _er -> cons(b, cons(b, _uhzca_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 18, which took 4.147889 s (model generation: 3.694368, model checking: 0.453521): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ insert(x_0_0, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) /\ leq(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) /\ leq(x_0_0, x_2_0) /\ leq(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) /\ sort(x_0_1, 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_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_0_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= leq(x_1_0, x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ sort(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) /\ leq(x_1_0, x_2_0) /\ sort(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(b, nil) ; h1 -> b ; l2 -> cons(b, _adfda_1) ; t1 -> nil } False <= leq(b, a) : No: () ------------------------------------------- Step 19, which took 6.914404 s (model generation: 4.497944, model checking: 2.416460): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_2(x_2_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_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) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_2(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= leq(x_1_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_2(x_2_1) /\ _r_3(x_1_0) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(b, nil) ; _er -> cons(a, cons(a, cons(_ubjja_0, nil))) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 20, which took 5.107352 s (model generation: 4.177718, model checking: 0.929634): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(b, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_0, x_2_1) /\ _r_1(x_1_0, x_2_1) /\ _r_2(x_0_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_1_0) /\ append(x_0_1, x_1_1, x_2_1) /\ insert(x_0_0, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_1(x_1_0, x_2_1) /\ _r_2(x_0_1) /\ _r_2(x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ leq(x_0_0, x_1_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_2_0) /\ sort(x_0_1, 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_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= leq(x_1_0, x_2_0) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ sort(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_1_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ sort(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ sort(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_1_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_2_0) /\ _r_4(x_1_0) /\ sort(x_1_1, x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= True _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) _r_1(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> nil ; _or -> nil ; _pr -> cons(a, nil) ; l -> nil } False <= leq(b, a) : No: () ------------------------------------------- Step 21, which took 8.215099 s (model generation: 8.209904, model checking: 0.005195): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(b, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) } Current best model: |_ name: None append -> [ append : { _r_1(b, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) append(nil, nil, nil) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(b, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_0) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(b, a) <= True _r_1(b, b) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_tuxma_0, cons(a, cons(b, _xoyma_1))) } insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(a, cons(b, cons(a, _ruyma_1))) ; h1 -> a ; l2 -> nil ; t1 -> cons(a, cons(_xryma_0, cons(a, _tuyma_1))) } eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) : Yes: { _nr -> cons(b, cons(a, _gpyma_1)) ; _or -> cons(a, nil) ; _pr -> cons(a, _nzxma_1) ; l -> cons(a, nil) } insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) : No: () sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) : Yes: { _dr -> cons(_hhyma_0, cons(a, _gpyma_1)) ; _er -> cons(a, cons(a, _auyma_1)) ; y -> a ; z -> cons(b, cons(a, _xqyma_1)) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () ------------------------------------------- Step 22, which took 10.973306 s (model generation: 6.467989, model checking: 4.505317): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, cons(b, nil))), cons(a, cons(a, cons(b, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True append(cons(a, cons(a, cons(a, cons(a, nil)))), nil, cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(b, cons(a, nil)))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(b, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_1) /\ _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_2(x_0_1) /\ _r_3(x_2_0) /\ append(x_0_1, x_1_1, x_2_1) /\ leq(x_0_0, x_1_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_3(x_2_0) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ sort(x_0_1, x_1_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= sort(x_1_1, x_2_1) append(nil, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) append(nil, nil, nil) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_2_1) /\ _r_3(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_0) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ sort(x_1_1, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_2(x_1_1) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= _r_2(x_0_1) /\ _r_3(x_0_0) _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(a) <= True _r_4(b) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_3(x_1_0) /\ _r_4(x_0_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ leq(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> b ; z -> cons(a, cons(a, _fhwta_1)) } False <= leq(b, a) : No: () ------------------------------------------- Step 23, which took 8.705486 s (model generation: 8.372349, model checking: 0.333137): Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, cons(b, nil))), cons(a, cons(a, cons(b, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, cons(a, nil))), cons(a, cons(b, cons(a, cons(a, nil))))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True append(cons(a, cons(a, cons(a, cons(a, nil)))), nil, cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(b, cons(a, nil)))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(b, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_0, x_2_1) /\ _r_3(x_0_1) /\ insert(x_0_0, x_1_1, x_2_1) /\ sort(x_0_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_1_1) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_0_1, x_1_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_0_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_1_1, 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_1) /\ _r_2(x_0_1) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, 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_1) /\ _r_3(x_0_1) /\ _r_3(x_2_1) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: append(nil, l2, l2) <= True : No: () insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) : Yes: { _ir -> cons(a, nil) ; h1 -> b ; l2 -> cons(_fahua_0, nil) ; t1 -> cons(_gahua_0, _gahua_1) } False <= leq(b, a) : No: () Total time: 60.054064 Learner time: 48.195190 Teacher time: 8.729792 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 append(cons(h1, t1), l2, cons(h1, _ir)) <= append(t1, l2, _ir) -> 0 eq_eltlist(_nr, _pr) <= append(cons(a, nil), _or, _pr) /\ sort(l, _or) /\ sort(cons(a, l), _nr) -> 0 insert(x, cons(y, z), cons(y, _yq)) \/ leq(x, y) <= insert(x, z, _yq) -> 0 sort(cons(y, z), _er) <= insert(y, _dr, _er) /\ sort(z, _dr) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), cons(b, nil), cons(b, cons(b, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, cons(a, cons(b, nil))), cons(a, cons(a, cons(b, nil)))) <= True append(nil, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True append(nil, cons(a, cons(b, cons(b, nil))), cons(a, cons(b, cons(b, nil)))) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True insert(a, cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= True insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, cons(a, cons(a, nil))), cons(a, cons(b, cons(a, cons(a, nil))))) <= True insert(a, cons(b, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True append(cons(a, cons(a, cons(a, cons(a, nil)))), nil, cons(a, cons(a, cons(b, cons(a, nil))))) <= append(cons(a, cons(a, cons(a, nil))), nil, cons(a, cons(b, cons(a, nil)))) False <= append(cons(a, nil), cons(a, cons(a, nil)), cons(a, nil)) /\ sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(a, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, 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, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, nil)) /\ sort(cons(b, nil), cons(a, nil)) False <= append(cons(a, nil), cons(b, nil), cons(b, nil)) /\ sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, cons(a, cons(a, nil)))) False <= append(cons(a, nil), nil, cons(b, nil)) append(cons(a, cons(b, cons(a, nil))), nil, cons(a, cons(b, nil))) <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) append(cons(b, cons(b, cons(b, nil))), nil, cons(b, cons(b, cons(a, nil)))) <= append(cons(b, cons(b, nil)), nil, cons(b, cons(a, nil))) append(cons(a, cons(b, nil)), cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= append(cons(b, nil), cons(a, cons(a, nil)), cons(a, nil)) append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(a, nil), cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= append(nil, cons(b, 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, nil, cons(a, nil)) sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= insert(a, cons(a, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) False <= insert(a, cons(a, nil), cons(a, nil)) sort(cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(b, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(nil, cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) <= insert(a, cons(b, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(b, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) insert(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(b, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, nil)) <= insert(b, cons(a, nil), cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, cons(a, nil)))) <= insert(b, nil, cons(a, cons(a, nil))) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(b, cons(a, nil))) <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ sort(cons(b, nil), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) False <= sort(cons(a, nil), nil) } Current best model: |_ name: None append -> [ append : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_1(x_0_0, x_2_1) /\ _r_3(x_0_1) /\ insert(x_0_0, x_1_1, x_2_1) /\ sort(x_0_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_1_1) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_0_1, x_1_1) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ append(x_0_1, x_1_1, x_2_1) /\ sort(x_0_1, x_2_1) /\ sort(x_1_1, x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_1_1, 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_1) /\ _r_2(x_0_1) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, 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_1) /\ _r_3(x_0_1) /\ _r_3(x_2_1) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_4(x_2_0) /\ sort(x_0_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_2_0) /\ leq(x_0_0, x_2_0) /\ sort(x_0_1, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ sort(x_1_1, x_2_1) append(nil, nil, nil) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; insert -> [ insert : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ sort(x_1_1, x_2_1) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_0_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ _r_2(x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_1) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= True sort(nil, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _|