Solving ../../benchmarks/smtlib/true/length_delete_minus_count.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: { elist -> {econs, enil} ; elt -> {a, b} ; nat -> {s, z} } definition: { (length_elt, F: { length_elt(enil, z) <= True length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) } eq_nat(_oka, _pka) <= length_elt(_nka, _oka) /\ length_elt(_nka, _pka) ) (minus, F: { minus(s(u), z, s(u)) <= True minus(z, y, z) <= True minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) } eq_nat(_tka, _uka) <= minus(_rka, _ska, _tka) /\ minus(_rka, _ska, _uka) ) (delete_all_elt, F: { delete_all_elt(x, enil, enil) <= True delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) } eq_elist(_zka, _ala) <= delete_all_elt(_xka, _yka, _ala) /\ delete_all_elt(_xka, _yka, _zka) ) (count_elt, F: { count_elt(x, enil, z) <= True count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) } eq_nat(_fla, _gla) <= count_elt(_dla, _ela, _fla) /\ count_elt(_dla, _ela, _gla) ) } properties: { eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) } over-approximation: {count_elt, delete_all_elt, length_elt, minus} under-approximation: {} Clause system for inference is: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Solving took 59.442734 seconds. Maybe: timeout during learnerLast solver state: Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, econs(a, enil)), s(s(z))) <= True count_elt(a, econs(a, econs(b, enil)), s(z)) <= True count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, econs(a, enil))), s(s(z))) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), s(s(z))) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, econs(a, enil)), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) count_elt(b, econs(b, econs(a, econs(a, enil))), s(s(z))) <= count_elt(b, econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(s(z))) count_elt(b, econs(a, econs(b, econs(b, enil))), s(s(z))) <= count_elt(b, econs(b, econs(b, enil)), s(s(z))) count_elt(b, econs(a, econs(b, enil)), s(s(z))) <= count_elt(b, econs(b, enil), s(s(z))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_1_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) /\ length_elt(x_1_1, x_2_0) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_5(x_1_1) /\ length_elt(x_1_1, x_2_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005619 s (model generation: 0.005477, model checking: 0.000142): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None count_elt -> [ count_elt : { } ] ; delete_all_elt -> [ delete_all_elt : { } ] ; length_elt -> [ length_elt : { } ] ; minus -> [ minus : { } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : Yes: { x -> b } delete_all_elt(x, enil, enil) <= True : Yes: { x -> b } length_elt(enil, z) <= True : Yes: { } minus(s(u), z, s(u)) <= True : Yes: { } minus(z, y, z) <= True : Yes: { y -> z } eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : No: () count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 1, which took 0.010094 s (model generation: 0.009871, model checking: 0.000223): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(b, enil, z) <= True delete_all_elt(b, enil, enil) <= True length_elt(enil, z) <= True minus(s(z), z, s(z)) <= True minus(z, z, z) <= True } Current best model: |_ name: None count_elt -> [ count_elt : { count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(enil, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : Yes: { x -> a } delete_all_elt(x, enil, enil) <= True : Yes: { x -> a } length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : Yes: { y -> s(_qziq_0) } eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : No: () count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> z ; t1 -> enil ; x -> b } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> z ; h1 -> a ; t1 -> enil ; x -> b } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> enil ; h -> b ; t -> enil } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : Yes: { _wka -> enil ; h -> a ; t -> enil ; x -> b } length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : Yes: { _mka -> z ; ll -> enil } minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : Yes: { _qka -> z ; u -> z ; x2 -> z } ------------------------------------------- Step 2, which took 0.017010 s (model generation: 0.016714, model checking: 0.000296): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, enil, z) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True } Current best model: |_ name: None count_elt -> [ count_elt : { count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(_dbjq_0) ; _kla -> z ; _lla -> s(_fbjq_0) ; e -> b ; l -> econs(_hbjq_0, _hbjq_1) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> z ; t1 -> enil ; x -> a } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> z ; h1 -> b ; t1 -> enil ; x -> a } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> enil ; h -> a ; t -> enil } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : Yes: { _wka -> enil ; h -> b ; t -> enil ; x -> a } length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : Yes: { _qka -> s(_wbjq_0) ; u -> s(_xbjq_0) ; x2 -> z } ------------------------------------------- Step 3, which took 0.023960 s (model generation: 0.023698, model checking: 0.000262): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= delete_all_elt(b, econs(a, enil), enil) } Current best model: |_ name: None count_elt -> [ count_elt : { count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_1(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_1(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= True minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(_pcjq_0) ; _kla -> s(_qcjq_0) ; _lla -> s(_rcjq_0) ; e -> a ; l -> econs(_tcjq_0, _tcjq_1) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 4, which took 0.037337 s (model generation: 0.037072, model checking: 0.000265): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= delete_all_elt(b, econs(a, enil), enil) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(_bgjq_0) ; _kla -> z ; _lla -> s(_dgjq_0) ; e -> a ; l -> econs(_fgjq_0, _fgjq_1) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 5, which took 0.029031 s (model generation: 0.028754, model checking: 0.000277): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= delete_all_elt(b, econs(a, enil), enil) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(b) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_rjjq_0, _rjjq_1) ; _ila -> s(_sjjq_0) ; _jla -> s(_tjjq_0) ; _kla -> s(_ujjq_0) ; _lla -> z ; e -> b ; l -> econs(_xjjq_0, _xjjq_1) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 6, which took 0.027940 s (model generation: 0.027582, model checking: 0.000358): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, enil), s(z)) False <= delete_all_elt(b, econs(a, enil), enil) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(b) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_uljq_0, _uljq_1) ; _ila -> s(_vljq_0) ; _jla -> s(_wljq_0) ; _kla -> s(_xljq_0) ; _lla -> z ; e -> a ; l -> econs(_amjq_0, _amjq_1) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(_wojq_0) ; h1 -> a ; t1 -> econs(b, _yojq_1) ; x -> b } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 7, which took 0.048529 s (model generation: 0.048042, model checking: 0.000487): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, enil), s(z)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(b) <= True _r_3(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(s(_dvjq_0)) ; _kla -> s(_eqjq_0) ; _lla -> s(_fqjq_0) ; e -> a ; l -> econs(_hqjq_0, _hqjq_1) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> econs(_cujq_0, _cujq_1) ; h -> a ; t -> econs(b, _eujq_1) } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 8, which took 0.055576 s (model generation: 0.055000, model checking: 0.000576): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, enil), s(z)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(b) <= True _r_3(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(z) ; _kla -> z ; _lla -> s(_qyjq_0) ; e -> b ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 9, which took 0.088467 s (model generation: 0.087910, model checking: 0.000557): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) /\ length_elt(econs(b, enil), s(z)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= True count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { _r_2(a, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(a, _rdkq_1) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> s(_udkq_0) ; _lla -> z ; e -> b ; l -> econs(a, econs(_ghkq_0, _ghkq_1)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : Yes: { _mka -> z ; ll -> enil ; x -> b } minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : Yes: { _qka -> s(_ugkq_0) ; u -> s(s(_ehkq_0)) ; x2 -> s(z) } ------------------------------------------- Step 10, which took 0.124025 s (model generation: 0.123386, model checking: 0.000639): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(z) ; _kla -> z ; _lla -> s(_oikq_0) ; e -> a ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 11, which took 0.125493 s (model generation: 0.124808, model checking: 0.000685): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(a) <= True _r_3(b) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(b, enil) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> s(_bokq_0) ; _lla -> z ; e -> a ; l -> econs(_eokq_0, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 12, which took 0.125915 s (model generation: 0.125281, model checking: 0.000634): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(b) <= True _r_3(a) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True _r_3(a) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_2(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= True delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_xvkq_0, enil) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> s(_awkq_0) ; _lla -> z ; e -> b ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> econs(b, _ezkq_1) ; h -> a ; t -> econs(b, _gzkq_1) } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 13, which took 0.134839 s (model generation: 0.134015, model checking: 0.000824): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_tblq_0, enil) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> s(_wblq_0) ; _lla -> z ; e -> a ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> econs(_qhlq_0, _qhlq_1) ; h -> b ; t -> econs(a, _shlq_1) } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 14, which took 0.165934 s (model generation: 0.164804, model checking: 0.001130): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) /\ delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(b) <= True _r_3(a) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(b) <= True _r_3(a) <= True _r_4(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_smlq_0, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> s(_vmlq_0) ; _lla -> z ; e -> b ; l -> econs(b, econs(_dulq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(_fqlq_0) ; h1 -> b ; t1 -> econs(a, _hqlq_1) ; x -> a } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 15, which took 0.194619 s (model generation: 0.192647, model checking: 0.001972): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) /\ delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(z)) /\ length_elt(econs(b, econs(a, enil)), s(s(z))) /\ minus(s(s(z)), s(z), z) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) /\ _r_4(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) /\ length_elt(x_1_1, x_2_0) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) count_elt(b, enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_xwlq_0, enil) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> z ; _lla -> s(s(_gjmq_0)) ; e -> a ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> z ; t1 -> econs(a, _tcmq_1) ; x -> b } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 16, which took 0.343684 s (model generation: 0.342372, model checking: 0.001312): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) /\ delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), econs(a, enil)) /\ minus(s(z), z, s(s(z))) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= length_elt(econs(b, econs(a, enil)), s(s(z))) /\ minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= True count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { _r_1(enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(b, enil) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> s(_rkmq_0) ; _lla -> z ; e -> a ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : Yes: { _mka -> s(z) ; ll -> econs(_jumq_0, enil) } minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 17, which took 0.417175 s (model generation: 0.415732, model checking: 0.001443): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), econs(a, enil)) /\ minus(s(z), z, s(s(z))) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= length_elt(econs(b, econs(a, enil)), s(s(z))) /\ minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_nbnq_0, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> z ; _lla -> s(s(_qinq_0)) ; e -> b ; l -> econs(a, econs(_rinq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : Yes: { _qka -> z ; u -> s(z) ; x2 -> s(_ohnq_0) } ------------------------------------------- Step 18, which took 0.401406 s (model generation: 0.399968, model checking: 0.001438): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), z) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ minus(s(s(z)), z, s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), econs(a, enil)) /\ minus(s(z), z, s(s(z))) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= length_elt(econs(b, econs(a, enil)), s(s(z))) /\ minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : Yes: { u -> s(_bxnq_0) } minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_vjnq_0, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> s(s(_cxnq_0)) ; _lla -> z ; e -> a ; l -> econs(a, econs(_nxnq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 19, which took 0.416996 s (model generation: 0.412610, model checking: 0.004386): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) /\ length_elt(econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), z) /\ delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), econs(a, enil)) /\ minus(s(z), z, s(s(z))) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= length_elt(econs(b, econs(a, enil)), s(s(z))) /\ minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(a) <= True _r_3(b) <= True _r_4(enil) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_2(x_1_0) /\ _r_4(x_1_1) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(a) <= True _r_3(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_2(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { _r_2(a) <= True _r_4(enil) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_0) /\ length_elt(x_0_1, x_1_0) length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) /\ length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= True minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_eqoq_0, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> s(_hqoq_0) ; _lla -> z ; e -> b ; l -> econs(a, econs(a, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> z ; h1 -> a ; t1 -> econs(a, enil) ; x -> b } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : Yes: { _mka -> s(z) ; ll -> econs(a, enil) ; x -> b } minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 20, which took 0.763069 s (model generation: 0.760795, model checking: 0.002274): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), econs(a, enil)) /\ minus(s(z), z, s(s(z))) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True _r_6(enil) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= True minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(b, enil) ; _ila -> s(z) ; _jla -> s(z) ; _kla -> z ; _lla -> s(s(_yaqq_0)) ; e -> a ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : Yes: { _wka -> enil ; h -> a ; t -> econs(b, _lypq_1) ; x -> b } length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 21, which took 1.315429 s (model generation: 1.313655, model checking: 0.001774): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_4(a) <= True _r_5(b) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_5(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_2(econs(x_0_0, x_0_1), enil) <= _r_5(x_0_0) _r_2(enil, enil) <= True _r_4(a) <= True _r_5(b) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_1) /\ _r_4(x_1_0) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_5(x_1_0) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_3(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_3(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0, x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0, x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(s(z)) ; _kla -> s(_xfqq_0) ; _lla -> s(_yfqq_0) ; e -> b ; l -> econs(b, econs(_trqq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> econs(_mkqq_0, econs(_orqq_0, _orqq_1)) ; h -> a ; t -> econs(b, _okqq_1) } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : Yes: { _wka -> econs(_lnqq_0, enil) ; h -> a ; t -> econs(a, enil) ; x -> b } length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : Yes: { _qka -> z ; u -> z ; x2 -> s(_mqqq_0) } ------------------------------------------- Step 22, which took 1.025196 s (model generation: 1.021782, model checking: 0.003414): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True _r_6(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_6(enil) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_jzqq_0, econs(_trrq_0, enil)) ; _ila -> s(s(z)) ; _jla -> s(z) ; _kla -> s(s(_rqrq_0)) ; _lla -> z ; e -> b ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 23, which took 1.299622 s (model generation: 1.295993, model checking: 0.003629): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), s(s(z))) /\ delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(b) <= True _r_4(a) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(b, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> s(s(_hvsq_0)) ; _lla -> z ; e -> a ; l -> econs(b, econs(_uvsq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 24, which took 1.253069 s (model generation: 1.247295, model checking: 0.005774): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), s(s(z))) /\ delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= True _r_6(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_6(enil) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_4(x_2_0) /\ _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_5(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(s(z)) ; _kla -> s(_cysq_0) ; _lla -> s(_dysq_0) ; e -> a ; l -> econs(a, econs(_teuq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : Yes: { _wka -> enil ; h -> b ; t -> econs(a, _dutq_1) ; x -> a } length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 25, which took 3.711973 s (model generation: 3.708831, model checking: 0.003142): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, econs(a, enil)), s(z)) /\ delete_all_elt(a, econs(a, econs(a, enil)), enil) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), s(s(z))) /\ delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(z) <= True _r_3(b) <= True _r_4(a) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_mpuq_0, econs(_ffvq_0, enil)) ; _ila -> s(s(z)) ; _jla -> s(s(z)) ; _kla -> s(s(_tevq_0)) ; _lla -> z ; e -> b ; l -> econs(_spuq_0, econs(_hfvq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> s(z) ; t1 -> econs(_isuq_0, econs(_dfvq_0, _dfvq_1)) ; x -> a } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : No: () delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : Yes: { _vka -> enil ; h -> a ; t -> econs(a, enil) } eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 26, which took 7.643618 s (model generation: 7.639228, model checking: 0.004390): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(s(z))) /\ delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, enil), s(s(z))) /\ delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(z) <= True _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_3(x_1_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_movq_0, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> s(s(_dlwq_0)) ; _lla -> z ; e -> b ; l -> econs(b, econs(_emwq_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> s(_jtvq_0) ; t1 -> econs(a, enil) ; x -> a } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(s(_alwq_0)) ; h1 -> a ; t1 -> econs(b, _wyvq_1) ; x -> b } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 27, which took 3.357358 s (model generation: 3.353600, model checking: 0.003758): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, econs(a, enil)), s(s(z))) <= True count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(s(z))) count_elt(b, econs(a, econs(b, enil)), s(s(z))) <= count_elt(b, econs(b, enil), s(s(z))) False <= count_elt(b, econs(b, enil), s(s(z))) /\ delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_2(z) <= True _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ length_elt(x_1_1, x_2_0) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_1_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= True _r_6(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_6(enil) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_5(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_5(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(_muwq_0, econs(_nsxq_0, enil)) ; _ila -> s(s(z)) ; _jla -> s(z) ; _kla -> s(z) ; _lla -> z ; e -> b ; l -> econs(b, enil) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> s(z) ; t1 -> econs(_ucxq_0, econs(_csxq_0, _csxq_1)) ; x -> b } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(s(z)) ; h1 -> b ; t1 -> econs(a, econs(_zsxq_0, enil)) ; x -> a } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 28, which took 14.932672 s (model generation: 14.921422, model checking: 0.011250): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, econs(a, enil)), s(s(z))) <= True count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, econs(a, enil))), s(s(z))) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) count_elt(b, econs(b, econs(a, econs(a, enil))), s(s(z))) <= count_elt(b, econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(s(z))) count_elt(b, econs(a, econs(b, enil)), s(s(z))) <= count_elt(b, econs(b, enil), s(s(z))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(z) <= True _r_2(s(x_0_0)) <= True _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_3(x_1_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_4(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) /\ _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> enil ; _ila -> z ; _jla -> s(s(z)) ; _kla -> s(s(_xzzq_0)) ; _lla -> s(_kxxq_0) ; e -> a ; l -> econs(a, econs(_pcar_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> s(s(_rcar_0)) ; t1 -> econs(a, enil) ; x -> b } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(s(_ybar_0)) ; h1 -> a ; t1 -> econs(a, enil) ; x -> b } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 29, which took 10.921231 s (model generation: 10.909530, model checking: 0.011701): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, econs(a, enil)), s(s(z))) <= True count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, econs(a, enil))), s(s(z))) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) count_elt(b, econs(b, econs(a, econs(a, enil))), s(s(z))) <= count_elt(b, econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(s(z))) count_elt(b, econs(a, econs(b, enil)), s(s(z))) <= count_elt(b, econs(b, enil), s(s(z))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_1_0) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_3(x_1_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) /\ _r_5(x_1_1) /\ length_elt(x_1_1, x_2_0) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(b, enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(econs(x_0_0, x_0_1), z) <= True length_elt(enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(b) <= True _r_4(a) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_6(x_1_1) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(econs(x_0_0, x_0_1), z) <= True length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= True _r_2(s(x_0_0)) <= _r_1(x_0_0) _r_2(z) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_1_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_0_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_2_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(b, enil) ; _ila -> s(z) ; _jla -> z ; _kla -> z ; _lla -> z ; e -> a ; l -> econs(b, econs(_lzcr_0, _lzcr_1)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : No: () eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(s(z)) ; h1 -> b ; t1 -> econs(a, enil) ; x -> a } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () ------------------------------------------- Step 30, which took 9.408819 s (model generation: 9.395734, model checking: 0.013085): Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, econs(a, enil)), s(s(z))) <= True count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, econs(a, enil))), s(s(z))) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), s(s(z))) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, econs(a, enil)), z) /\ length_elt(econs(b, econs(a, enil)), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) count_elt(b, econs(b, econs(a, econs(a, enil))), s(s(z))) <= count_elt(b, econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(s(z))) count_elt(b, econs(a, econs(b, enil)), s(s(z))) <= count_elt(b, econs(b, enil), s(s(z))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_1_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) /\ length_elt(x_1_1, x_2_0) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_5(x_1_1) /\ length_elt(x_1_1, x_2_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _| Answer of teacher: count_elt(x, enil, z) <= True : No: () delete_all_elt(x, enil, enil) <= True : No: () length_elt(enil, z) <= True : No: () minus(s(u), z, s(u)) <= True : No: () minus(z, y, z) <= True : No: () eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) : Yes: { _hla -> econs(b, enil) ; _ila -> s(z) ; _jla -> s(s(z)) ; _kla -> z ; _lla -> s(s(_rwfr_0)) ; e -> a ; l -> econs(b, econs(_fyfr_0, enil)) } count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) : Yes: { _bla -> z ; t1 -> econs(b, _hher_1) ; x -> a } eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) : Yes: { _cla -> s(s(z)) ; h1 -> a ; t1 -> econs(b, econs(b, _dbgr_1)) ; x -> b } delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) : No: () eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) : No: () length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) : No: () minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) : No: () Total time: 59.442734 Learner time: 58.343608 Teacher time: 0.082098 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { count_elt(x, enil, z) <= True -> 0 delete_all_elt(x, enil, enil) <= True -> 0 length_elt(enil, z) <= True -> 0 minus(s(u), z, s(u)) <= True -> 0 minus(z, y, z) <= True -> 0 eq_nat(_ila, _lla) <= count_elt(e, l, _kla) /\ delete_all_elt(e, l, _hla) /\ length_elt(_hla, _ila) /\ length_elt(l, _jla) /\ minus(_jla, _kla, _lla) -> 0 count_elt(x, econs(x, t1), s(_bla)) <= count_elt(x, t1, _bla) -> 0 eq_elt(h1, x) \/ count_elt(x, econs(h1, t1), _cla) <= count_elt(x, t1, _cla) -> 0 delete_all_elt(h, econs(h, t), _vka) <= delete_all_elt(h, t, _vka) -> 0 eq_elt(x, h) \/ delete_all_elt(x, econs(h, t), econs(h, _wka)) <= delete_all_elt(x, t, _wka) -> 0 length_elt(econs(x, ll), s(_mka)) <= length_elt(ll, _mka) -> 0 minus(s(u), s(x2), _qka) <= minus(u, x2, _qka) -> 0 } Accumulated learning constraints: { count_elt(a, econs(a, econs(a, enil)), s(s(z))) <= True count_elt(a, econs(a, econs(b, enil)), s(z)) <= True count_elt(a, econs(a, enil), s(z)) <= True count_elt(a, econs(b, econs(a, econs(a, enil))), s(s(z))) <= True count_elt(a, econs(b, econs(a, enil)), s(z)) <= True count_elt(a, econs(b, enil), z) <= True count_elt(a, enil, z) <= True count_elt(b, econs(a, econs(a, enil)), z) <= True count_elt(b, econs(a, econs(b, enil)), s(z)) <= True count_elt(b, econs(a, enil), z) <= True count_elt(b, econs(b, econs(a, enil)), s(z)) <= True count_elt(b, econs(b, enil), s(z)) <= True count_elt(b, enil, z) <= True delete_all_elt(a, econs(a, econs(a, enil)), enil) <= True delete_all_elt(a, econs(a, econs(b, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(a, enil), enil) <= True delete_all_elt(a, econs(b, econs(a, enil)), econs(b, enil)) <= True delete_all_elt(a, econs(b, enil), econs(b, enil)) <= True delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(a, econs(a, enil)), econs(a, econs(a, enil))) <= True delete_all_elt(b, econs(a, econs(b, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(a, enil), econs(a, enil)) <= True delete_all_elt(b, econs(b, econs(a, enil)), econs(a, enil)) <= True delete_all_elt(b, econs(b, enil), enil) <= True delete_all_elt(b, enil, enil) <= True length_elt(econs(a, econs(a, enil)), s(s(z))) <= True length_elt(econs(a, enil), s(z)) <= True length_elt(econs(b, econs(a, enil)), s(s(z))) <= True length_elt(econs(b, enil), s(z)) <= True length_elt(enil, z) <= True minus(s(s(s(z))), s(s(z)), s(z)) <= True minus(s(s(z)), s(s(z)), z) <= True minus(s(s(z)), s(z), s(z)) <= True minus(s(s(z)), z, s(s(z))) <= True minus(s(z), s(s(z)), z) <= True minus(s(z), s(z), z) <= True minus(s(z), z, s(z)) <= True minus(z, s(z), z) <= True minus(z, z, z) <= True False <= count_elt(a, econs(a, econs(a, enil)), s(z)) False <= count_elt(a, econs(a, enil), s(s(z))) False <= count_elt(a, econs(a, enil), z) False <= count_elt(a, econs(b, econs(a, enil)), s(s(z))) False <= count_elt(a, econs(b, econs(a, enil)), z) False <= count_elt(a, econs(b, enil), s(z)) False <= count_elt(b, econs(a, econs(a, enil)), s(s(z))) count_elt(b, econs(b, econs(a, econs(a, enil))), s(s(z))) <= count_elt(b, econs(a, econs(a, enil)), s(z)) False <= count_elt(b, econs(a, enil), s(s(z))) False <= count_elt(b, econs(a, enil), s(z)) False <= count_elt(b, econs(b, econs(a, enil)), s(s(z))) count_elt(b, econs(a, econs(b, econs(b, enil))), s(s(z))) <= count_elt(b, econs(b, econs(b, enil)), s(s(z))) count_elt(b, econs(a, econs(b, enil)), s(s(z))) <= count_elt(b, econs(b, enil), s(s(z))) False <= count_elt(b, econs(b, enil), z) False <= delete_all_elt(a, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(a, enil)) False <= delete_all_elt(a, econs(a, enil), econs(b, enil)) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, econs(a, enil))) <= delete_all_elt(a, econs(b, enil), econs(a, econs(a, enil))) delete_all_elt(a, econs(a, econs(b, enil)), econs(a, enil)) <= delete_all_elt(a, econs(b, enil), econs(a, enil)) False <= delete_all_elt(a, econs(b, enil), enil) False <= delete_all_elt(b, econs(a, econs(a, enil)), econs(a, enil)) False <= delete_all_elt(b, econs(a, enil), enil) False <= delete_all_elt(b, econs(b, econs(a, enil)), enil) False <= delete_all_elt(b, econs(b, enil), econs(a, econs(a, enil))) False <= delete_all_elt(b, econs(b, enil), econs(a, enil)) False <= length_elt(econs(a, enil), s(s(z))) False <= minus(s(s(z)), s(s(z)), s(z)) False <= minus(s(s(z)), s(z), z) False <= minus(s(z), s(z), s(z)) False <= minus(s(z), z, s(s(z))) } Current best model: |_ name: None count_elt -> [ count_elt : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_1_0) /\ _r_6(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(a, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) /\ length_elt(x_1_1, x_2_0) count_elt(a, econs(x_1_0, x_1_1), z) <= _r_4(x_1_0) count_elt(a, enil, z) <= True count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_6(x_1_1) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_2_0) /\ _r_5(x_1_1) /\ length_elt(x_1_1, x_2_0) count_elt(b, econs(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) /\ _r_5(x_1_1) count_elt(b, econs(x_1_0, x_1_1), z) <= _r_3(x_1_0) count_elt(b, enil, z) <= True length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; delete_all_elt -> [ delete_all_elt : { _r_3(a) <= True _r_4(b) <= True _r_5(econs(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_5(econs(x_0_0, x_0_1)) <= _r_6(x_0_1) _r_5(enil) <= True _r_6(econs(x_0_0, x_0_1)) <= True delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all_elt(a, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ _r_6(x_1_1) delete_all_elt(a, econs(x_1_0, x_1_1), enil) <= _r_3(x_1_0) delete_all_elt(a, enil, enil) <= True delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_6(x_2_1) delete_all_elt(b, econs(x_1_0, x_1_1), econs(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_6(x_1_1) delete_all_elt(b, econs(x_1_0, x_1_1), enil) <= _r_4(x_1_0) /\ _r_5(x_1_1) delete_all_elt(b, enil, enil) <= True } ] ; length_elt -> [ length_elt : { length_elt(econs(x_0_0, x_0_1), s(x_1_0)) <= length_elt(x_0_1, x_1_0) length_elt(enil, z) <= True } ] ; minus -> [ minus : { _r_1(s(x_0_0)) <= _r_2(x_0_0) _r_1(z) <= True _r_2(s(x_0_0)) <= True minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_0_0) /\ _r_2(x_1_0) minus(s(x_0_0), s(x_1_0), s(x_2_0)) <= _r_1(x_1_0) /\ _r_2(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_1(x_0_0) minus(s(x_0_0), s(x_1_0), z) <= _r_2(x_1_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_1(x_2_0) minus(s(x_0_0), z, s(x_2_0)) <= _r_2(x_0_0) minus(z, s(x_1_0), z) <= True minus(z, z, z) <= True } ] -- Equality automata are defined for: {elist, elt, nat} _|