Solving ../../benchmarks/smtlib/true/sort_cons.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: Some(60.) (sec) Teacher_type: Checks all clauses every time Approximation method: remove every clause that can be safely removed Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} } definition: { (leq, P: { leq(a, y) <= True leq(b, b) <= True False <= leq(b, a) } ) (insert, F: { insert(x, nil, cons(x, nil)) <= True insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) } eq_eltlist(_noa, _ooa) <= insert(_loa, _moa, _noa) /\ insert(_loa, _moa, _ooa) ) (sort, F: { sort(nil, nil) <= True sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) } eq_eltlist(_soa, _toa) <= sort(_roa, _soa) /\ sort(_roa, _toa) ) } properties: { eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) } over-approximation: {insert, sort} under-approximation: {} Clause system for inference is: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Solving took 60.902113 seconds. Maybe: timeout during learnerLast solver state: Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(b, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, cons(a, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(a, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= 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 <= sort(cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_1_0) /\ _r_5(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_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(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_5(x_0_0) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_0_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) /\ _r_5(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006074 s (model generation: 0.005998, model checking: 0.000076): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None insert -> [ insert : { } ] ; leq -> [ leq : { } ] ; sort -> [ sort : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: 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: { } insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 1, which took 0.006358 s (model generation: 0.006274, model checking: 0.000084): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { insert(b, nil, cons(b, nil)) <= True leq(a, b) <= True leq(b, b) <= True sort(nil, nil) <= True } Current best model: |_ name: None 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} _| Answer of teacher: 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: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : Yes: { _koa -> cons(_mykva_0, _mykva_1) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(_rykva_0, _rykva_1) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> b ; y -> b } False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 2, which took 0.010066 s (model generation: 0.009883, model checking: 0.000183): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 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} _| 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> b } False <= leq(b, a) : Yes: { } eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(b, _fzkva_1) ; _voa -> nil ; l -> nil } ------------------------------------------- Step 3, which took 0.019700 s (model generation: 0.019540, model checking: 0.000160): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 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} _| 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(b, _uzkva_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(_talva_0, _talva_1)) ; _voa -> nil ; l -> nil } ------------------------------------------- Step 4, which took 0.015598 s (model generation: 0.015254, model checking: 0.000344): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 <= 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(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None 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(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(b, _ublva_1) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 5, which took 0.029038 s (model generation: 0.028886, model checking: 0.000152): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 <= 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(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None 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_2(b) <= True 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} _| 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(a, _tdlva_1) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 6, which took 0.037031 s (model generation: 0.036455, model checking: 0.000576): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 <= 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(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None 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(a, a) <= True _r_1(b, a) <= True _r_1(b, b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, nil) ; _qoa -> cons(b, _uelva_1) ; y -> a ; z -> cons(b, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(a, cons(a, nil))) ; _voa -> cons(b, cons(a, nil)) ; l -> cons(b, cons(a, nil)) } ------------------------------------------- Step 7, which took 0.045717 s (model generation: 0.044992, model checking: 0.000725): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) False <= leq(b, a) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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 insert -> [ insert : { _r_2(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _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} _| 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(b, cons(_dolva_0, _dolva_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(b, nil)) ; _voa -> cons(a, nil) ; l -> cons(b, _mnlva_1) } ------------------------------------------- Step 8, which took 0.048988 s (model generation: 0.047624, model checking: 0.001364): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(b, nil)) insert(b, cons(a, nil), cons(a, cons(a, nil))) <= insert(b, nil, cons(a, nil)) sort(cons(b, nil), cons(a, nil)) <= insert(b, nil, cons(a, nil)) 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) } Current best model: |_ name: None 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_1(x_2_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)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a) <= True _r_2(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_0) /\ _r_1(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) /\ _r_2(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(a, _etlva_1) ; y -> b ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(b, nil)) ; _voa -> cons(b, cons(_oylva_0, _oylva_1)) ; l -> cons(b, _xwlva_1) } ------------------------------------------- Step 9, which took 0.118049 s (model generation: 0.117678, model checking: 0.000371): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, 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 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(a, nil) <= True _r_1(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _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_1(x_0_0, x_1_1) /\ _r_2(x_0_0, x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(a, cons(_ldmva_0, _ldmva_1)) ; y -> a ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, nil) ; _voa -> cons(b, nil) ; l -> cons(b, _hdmva_1) } ------------------------------------------- Step 10, which took 0.107420 s (model generation: 0.106588, model checking: 0.000832): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, 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 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_1(nil) <= True _r_2(a) <= True _r_3(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_2(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(_mfmva_0, _mfmva_1) ; _qoa -> cons(a, cons(_ijmva_0, _ijmva_1)) ; y -> a ; z -> cons(b, _pfmva_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 11, which took 0.138099 s (model generation: 0.137084, model checking: 0.001015): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(a, nil), cons(a, 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(a, nil)) <= insert(b, cons(a, nil), 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, 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 insert -> [ insert : { _r_1(nil) <= True _r_2(a) <= True _r_3(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_0) /\ _r_3(x_1_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_1(nil) <= True _r_2(a) <= True _r_3(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_0_1) /\ _r_1(x_1_1) /\ _r_2(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, _nkmva_1) ; _qoa -> cons(a, cons(_nomva_0, _nomva_1)) ; y -> a ; z -> cons(b, _qkmva_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> a } False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 12, which took 0.139476 s (model generation: 0.138165, model checking: 0.001311): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, nil), cons(a, cons(a, nil))) False <= sort(cons(a, nil), cons(b, nil)) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _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) /\ 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_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), nil) <= True sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(b, cons(_gzmva_0, _gzmva_1)) ; y -> b ; z -> cons(_ptmva_0, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> nil ; _voa -> nil ; l -> nil } ------------------------------------------- Step 13, which took 0.163627 s (model generation: 0.160506, model checking: 0.003121): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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 sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, 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) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_1(nil) <= True _r_2(a) <= True _r_3(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_2(x_2_0) 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_1) /\ _r_2(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(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_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_0_0) /\ _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) /\ _r_3(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : Yes: { _koa -> cons(b, nil) ; x -> b ; y -> a ; z -> nil } sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> nil ; _qoa -> cons(b, cons(b, _ipnva_1)) ; y -> b ; z -> nil } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 14, which took 0.189776 s (model generation: 0.187304, model checking: 0.002472): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, 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) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _r_2(nil) <= True _r_3(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(a, 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)) <= 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_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_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} _| 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(a, cons(b, _giova_1)) ; y -> a ; z -> cons(_ounva_0, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(b, cons(a, nil)) ; _voa -> cons(_qeova_0, nil) ; l -> cons(b, nil) } ------------------------------------------- Step 15, which took 0.825939 s (model generation: 0.824367, model checking: 0.001572): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) 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(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, 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) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _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_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)) <= True 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_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) _r_1(cons(x_0_0, x_0_1), nil) <= _r_4(x_0_0) _r_1(nil, nil) <= True _r_2(a, a) <= True _r_2(b, a) <= True _r_2(b, b) <= True _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_1, x_1_1) /\ _r_2(x_0_0, x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, nil) ; _qoa -> cons(a, 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: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, nil) ; _voa -> cons(a, nil) ; l -> cons(a, nil) } ------------------------------------------- Step 16, which took 0.587209 s (model generation: 0.573661, model checking: 0.013548): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) 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, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, 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) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True 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_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_0_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, cons(_gzrva_0, _gzrva_1)) ; _qoa -> cons(_pjrva_0, cons(_dzrva_0, _dzrva_1)) ; y -> b ; z -> cons(a, cons(_gzrva_0, _gzrva_1)) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(b, cons(_gzrva_0, _gzrva_1)) ; _voa -> cons(b, nil) ; l -> cons(b, _zwrva_1) } ------------------------------------------- Step 17, which took 0.881884 s (model generation: 0.867385, model checking: 0.014499): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, 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, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_3(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(a) <= True _r_4(b) <= True 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_0_0) /\ _r_3(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_3(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(b, cons(_dluva_0, _dluva_1)) ; y -> a ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(b, _tluva_1)) ; _voa -> cons(a, nil) ; l -> cons(a, nil) } ------------------------------------------- Step 18, which took 0.740092 s (model generation: 0.738791, model checking: 0.001301): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { insert(a, cons(a, nil), cons(a, cons(a, nil))) <= True insert(a, cons(b, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, 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, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, 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(a, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= sort(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None insert -> [ insert : { _r_2(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) _r_2(a, nil) <= True _r_2(b, cons(x_1_0, x_1_1)) <= True _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_2(x_1_0, 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)) <= True insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(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(b, cons(x_1_0, x_1_1)) <= True _r_1(b, nil) <= True _r_2(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) _r_2(a, nil) <= True _r_2(b, cons(x_1_0, x_1_1)) <= True _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_2(x_0_0, 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} _| 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(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, nil) ; _qoa -> cons(a, cons(b, _puuva_1)) ; y -> a ; z -> cons(b, _emuva_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : Yes: { x -> a ; y -> a ; z -> cons(_qruva_0, _qruva_1) } False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(a, nil)) ; _voa -> cons(b, nil) ; l -> cons(b, _yquva_1) } ------------------------------------------- Step 19, which took 2.296692 s (model generation: 2.293751, model checking: 0.002941): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _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_5(x_1_0) _r_2(a, cons(x_1_0, x_1_1)) <= True _r_3(nil) <= True _r_4(a) <= True _r_5(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_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_1_0, x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_4(a) <= True _r_5(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(a, cons(_qkvva_0, _qkvva_1)) ; y -> b ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 20, which took 2.503105 s (model generation: 2.500039, model checking: 0.003066): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(a) <= True _r_5(b) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_1_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_5(x_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_4(a) <= True _r_5(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : Yes: { _koa -> cons(a, cons(b, _gdwva_1)) ; x -> b ; y -> a ; z -> cons(_ppvva_0, _ppvva_1) } sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(a, cons(b, _mdwva_1)) ; y -> b ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : No: () ------------------------------------------- Step 21, which took 4.369544 s (model generation: 4.356815, model checking: 0.012729): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_2(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) _r_2(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_3(nil) <= True _r_4(b) <= True _r_5(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_1) /\ _r_5(x_2_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, 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_5(x_2_0) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) } ] ; 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) <= True _r_1(nil, b) <= True _r_4(b) <= True _r_5(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_4(x_0_0) /\ _r_5(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_4(x_0_0) /\ sort(x_0_1, x_1_1) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) /\ sort(x_0_1, x_1_1) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(a, nil) ; _qoa -> cons(a, cons(a, cons(_rtyva_0, _rtyva_1))) ; y -> a ; z -> cons(a, nil) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(a, nil)) ; _voa -> cons(a, cons(_rxyva_0, _rxyva_1)) ; l -> cons(b, cons(_euyva_0, _euyva_1)) } ------------------------------------------- Step 22, which took 9.071049 s (model generation: 9.017787, model checking: 0.053262): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= 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 <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(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_3(x_2_1) /\ _r_4(x_1_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_5(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_5(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_3(x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_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_5(x_0_0) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(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_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) sort(nil, nil) <= True } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(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_0_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, cons(b, _jjhwa_1)) ; _qoa -> cons(b, cons(b, _ijhwa_1)) ; y -> a ; z -> cons(a, cons(b, _ykhwa_1)) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(b, cons(b, _jjhwa_1)) ; _voa -> cons(_tehwa_0, cons(b, _jjhwa_1)) ; l -> cons(b, cons(b, _ckhwa_1)) } ------------------------------------------- Step 23, which took 10.627801 s (model generation: 10.553727, model checking: 0.074074): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= 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 <= sort(cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(a) <= True _r_5(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) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_1_0) insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) /\ sort(x_1_1, x_2_1) 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_2(x_2_1) insert(b, nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_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_2(x_1_1) /\ _r_5(x_0_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) /\ _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_3(x_1_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_3(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_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(a) <= True _r_5(b) <= True sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_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) /\ _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_3(x_1_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) sort(nil, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, cons(b, _hdrwa_1)) ; _qoa -> cons(b, cons(b, _fdrwa_1)) ; y -> a ; z -> cons(b, _cxkwa_1) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(a, cons(b, _jerwa_1)) ; _voa -> cons(a, cons(b, _ierwa_1)) ; l -> cons(b, _zarwa_1) } ------------------------------------------- Step 24, which took 18.664762 s (model generation: 18.490876, model checking: 0.173886): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(b, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= 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 <= sort(cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_1_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_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(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) 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) 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_5(x_0_0) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) /\ _r_3(x_1_1) /\ _r_5(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) : Yes: { _uoa -> cons(b, cons(a, _otdxa_1)) ; _voa -> cons(a, cons(b, _stdxa_1)) ; l -> cons(a, cons(b, _yudxa_1)) } ------------------------------------------- Step 25, which took 8.242379 s (model generation: 8.110110, model checking: 0.132269): Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(b, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, 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(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(a, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= 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 <= sort(cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_1_0) /\ _r_5(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_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(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_5(x_0_0) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_0_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) /\ _r_5(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: insert(x, nil, cons(x, nil)) <= True : No: () leq(a, y) <= True : No: () leq(b, b) <= True : No: () sort(nil, nil) <= True : No: () insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) : No: () sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) : Yes: { _poa -> cons(b, _fqnxa_1) ; _qoa -> cons(b, cons(b, _qvuxa_1)) ; y -> a ; z -> cons(b, cons(a, _gvuxa_1)) } insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) : No: () False <= leq(b, a) : No: () Total time: 60.902113 Learner time: 59.389540 Teacher time: 0.495933 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { insert(x, nil, cons(x, nil)) <= True -> 0 leq(a, y) <= True -> 0 leq(b, b) <= True -> 0 sort(nil, nil) <= True -> 0 insert(x, cons(y, z), cons(y, _koa)) \/ leq(x, y) <= insert(x, z, _koa) -> 0 sort(cons(y, z), _qoa) <= insert(y, _poa, _qoa) /\ sort(z, _poa) -> 0 insert(x, cons(y, z), cons(x, cons(y, z))) <= leq(x, y) -> 0 False <= leq(b, a) -> 0 eq_eltlist(_uoa, cons(a, _voa)) <= sort(l, _voa) /\ sort(cons(a, l), _uoa) -> 0 } Accumulated learning constraints: { 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, nil), cons(a, cons(b, nil))) <= True insert(a, nil, cons(a, nil)) <= True insert(b, cons(a, cons(a, nil)), cons(a, cons(a, cons(b, nil)))) <= True insert(b, cons(a, nil), cons(a, cons(b, nil))) <= True insert(b, cons(b, nil), cons(b, cons(b, nil))) <= True insert(b, nil, cons(b, nil)) <= True leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True sort(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True sort(cons(a, nil), cons(a, nil)) <= True sort(cons(b, cons(a, nil)), cons(a, cons(b, nil))) <= True sort(cons(b, nil), cons(b, nil)) <= True sort(nil, nil) <= True sort(cons(a, cons(a, nil)), cons(a, cons(a, cons(a, nil)))) <= insert(a, cons(a, nil), cons(a, cons(a, cons(a, nil)))) False <= insert(a, cons(a, nil), cons(a, cons(b, nil))) sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) <= insert(a, cons(a, nil), cons(b, cons(a, nil))) sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) sort(cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= insert(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) /\ sort(cons(b, nil), cons(b, cons(b, nil))) False <= insert(a, cons(b, nil), cons(a, cons(a, nil))) False <= insert(a, cons(b, nil), cons(a, nil)) sort(cons(a, cons(b, cons(a, nil))), cons(b, cons(b, nil))) <= insert(a, cons(b, nil), cons(b, cons(b, nil))) /\ sort(cons(b, cons(a, nil)), cons(b, nil)) sort(cons(a, cons(b, nil)), cons(b, nil)) <= insert(a, cons(b, nil), cons(b, nil)) False <= insert(a, nil, cons(a, cons(a, nil))) False <= insert(a, nil, cons(b, nil)) sort(cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= insert(b, cons(a, nil), cons(a, cons(a, nil))) sort(cons(b, cons(a, nil)), cons(a, nil)) <= insert(b, cons(a, nil), cons(a, nil)) sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= insert(b, cons(a, nil), cons(b, cons(a, nil))) sort(cons(b, cons(a, cons(a, nil))), cons(a, cons(a, nil))) <= insert(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) /\ sort(cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= insert(b, nil, cons(a, nil)) False <= insert(b, nil, cons(b, cons(a, nil))) sort(cons(b, nil), cons(b, cons(b, nil))) <= insert(b, nil, cons(b, cons(b, nil))) False <= leq(b, a) False <= sort(cons(a, cons(a, cons(b, nil))), cons(b, cons(a, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(a, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, cons(a, nil))), cons(a, cons(a, cons(a, nil)))) /\ sort(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= 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 <= sort(cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) /\ sort(cons(b, cons(b, nil)), cons(a, cons(b, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, cons(a, nil))) False <= sort(cons(a, cons(b, nil)), cons(a, nil)) False <= sort(cons(a, cons(b, nil)), cons(b, 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) False <= sort(cons(b, nil), cons(a, cons(b, nil))) False <= sort(cons(b, nil), cons(a, nil)) False <= sort(cons(b, nil), cons(b, cons(a, nil))) } Current best model: |_ name: None insert -> [ insert : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True insert(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_1_0) /\ _r_5(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_1_0) insert(a, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) insert(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True insert(b, nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) } ] ; leq -> [ leq : { leq(a, a) <= True leq(a, b) <= True leq(b, b) <= True } ] ; sort -> [ sort : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(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_5(x_0_0) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_2(x_1_1) /\ _r_5(x_1_0) sort(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) /\ _r_4(x_0_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) /\ _r_5(x_1_0) sort(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _|