Solving ../../benchmarks/smtlib/true/list_delete_all_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: { elt -> {a, b} ; eltlist -> {cons, nil} ; nat -> {s, z} } definition: { (delete_one, F: { delete_one(x, nil, nil) <= True delete_one(y, cons(y, r), r) <= True eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) } eq_eltlist(_om, _pm) <= delete_one(_mm, _nm, _om) /\ delete_one(_mm, _nm, _pm) ) (delete_all, F: { delete_all(x, nil, nil) <= True eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) } eq_eltlist(_um, _vm) <= delete_all(_sm, _tm, _um) /\ delete_all(_sm, _tm, _vm) ) (leqnat, P: { leqnat(z, n2) <= True leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) False <= leqnat(s(nn1), z) } ) (count, F: { count(x, nil, z) <= True eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) } eq_nat(_an, _bn) <= count(_ym, _zm, _an) /\ count(_ym, _zm, _bn) ) } properties: { leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) } over-approximation: {count, delete_all, delete_one} under-approximation: {leqnat} Clause system for inference is: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Solving took 59.907152 seconds. Maybe: timeout during learnerLast solver state: Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, cons(a, nil))), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(s(z)), s(s(z))) <= True leqnat(s(z), s(s(z))) <= True leqnat(s(z), s(z)) <= True leqnat(z, s(z)) <= True leqnat(z, z) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, cons(b, cons(a, cons(a, nil)))), s(s(z))) /\ delete_all(a, cons(a, cons(b, cons(a, cons(a, nil)))), cons(a, nil)) /\ delete_one(a, cons(a, cons(b, cons(a, cons(a, nil)))), cons(a, nil)) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, cons(a, nil))), s(s(z))) /\ delete_all(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) False <= delete_all(a, cons(b, cons(a, cons(a, nil))), cons(b, nil)) /\ delete_one(a, cons(b, cons(a, cons(a, nil))), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(a, cons(b, cons(b, nil)), cons(b, nil)) <= delete_all(a, cons(b, nil), nil) delete_all(b, cons(b, cons(a, nil)), cons(b, nil)) <= delete_all(b, cons(a, nil), cons(b, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= delete_one(a, cons(a, nil), cons(a, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= delete_one(b, cons(a, nil), cons(b, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(a) <= True _r_6(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(a) <= True _r_6(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_6(x_1_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.008290 s (model generation: 0.008059, model checking: 0.000231): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None count -> [ count : { } ] ; delete_all -> [ delete_all : { } ] ; delete_one -> [ delete_one : { } ] ; leqnat -> [ leqnat : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : Yes: { x -> b } delete_all(x, nil, nil) <= True : Yes: { x -> b } delete_one(x, nil, nil) <= True : Yes: { x -> b } delete_one(y, cons(y, r), r) <= True : Yes: { r -> nil ; y -> b } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : No: () eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 1, which took 0.018303 s (model generation: 0.017956, model checking: 0.000347): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(b, nil, z) <= True delete_all(b, nil, nil) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True } Current best model: |_ name: None count -> [ count : { count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : Yes: { x -> a } delete_all(x, nil, nil) <= True : Yes: { x -> a } delete_one(x, nil, nil) <= True : Yes: { x -> a } delete_one(y, cons(y, r), r) <= True : Yes: { r -> nil ; y -> a } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> z ; l -> nil ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> z ; r -> nil ; x -> b ; y -> a } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> z ; r -> nil ; y -> b } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> nil ; x -> b ; y -> a } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> nil ; r -> nil ; y -> b } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> nil ; r -> nil ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 2, which took 0.023663 s (model generation: 0.023257, model checking: 0.000406): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(z, s(z)) <= True } Current best model: |_ name: None count -> [ count : { count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(z, s(x_1_0)) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : Yes: { r -> cons(_etfs_0, _etfs_1) ; y -> a } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(_ltfs_0) ; l -> cons(_mtfs_0, _mtfs_1) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> z ; r -> nil ; x -> a ; y -> b } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> z ; r -> nil ; y -> a } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> nil ; x -> a ; y -> b } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> nil ; r -> nil ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> nil ; r -> nil ; x -> a ; y -> b } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> s(_lufs_0) } leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 3, which took 0.015957 s (model generation: 0.015816, model checking: 0.000141): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) } Current best model: |_ name: None count -> [ count : { count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= True leqnat(z, s(x_1_0)) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : No: () eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : Yes: { nn1 -> z ; nn2 -> z } False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 4, which took 0.014827 s (model generation: 0.014728, model checking: 0.000099): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) leqnat(z, z) <= leqnat(s(z), s(z)) } Current best model: |_ name: None count -> [ count : { count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= True leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : No: () eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : Yes: { nn1 -> s(_qufs_0) ; nn2 -> z } False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 5, which took 0.014759 s (model generation: 0.014343, model checking: 0.000416): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) leqnat(s(z), z) <= leqnat(s(s(z)), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) } Current best model: |_ name: None count -> [ count : { count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= True leqnat(s(x_0_0), z) <= True leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : No: () eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : Yes: { } ------------------------------------------- Step 6, which took 0.023509 s (model generation: 0.023319, model checking: 0.000190): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_svfs_0)) ; l -> cons(_yufs_0, _yufs_1) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 7, which took 0.024568 s (model generation: 0.024249, model checking: 0.000319): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { _r_1(z) <= True leqnat(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_gxfs_0)) ; l -> cons(_hwfs_0, _hwfs_1) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> s(z) ; r -> cons(_owfs_0, _owfs_1) ; y -> a } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : Yes: { nn1 -> s(z) ; nn2 -> s(_xwfs_0) } leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 8, which took 0.020241 s (model generation: 0.019978, model checking: 0.000263): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_kzfs_0)) ; l -> cons(_xxfs_0, cons(_jzfs_0, _jzfs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> s(z) ; r -> cons(_ayfs_0, nil) ; x -> a ; y -> b } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> z ; r -> cons(_uyfs_0, _uyfs_1) ; y -> b } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 9, which took 0.043648 s (model generation: 0.043286, model checking: 0.000362): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_2(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_dcgs_0)) ; l -> cons(_tzfs_0, cons(_ccgs_0, _ccgs_1)) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> s(z) ; r -> cons(_kbgs_0, nil) ; y -> b } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 10, which took 0.045009 s (model generation: 0.044672, model checking: 0.000337): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= delete_all(a, cons(a, cons(a, nil)), nil) /\ delete_one(a, cons(a, cons(a, nil)), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(nil) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_qcgs_0, _qcgs_1) ; _en -> s(s(_vegs_0)) ; l -> cons(_scgs_0, cons(_uegs_0, _uegs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> nil ; r -> cons(_zdgs_0, nil) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 11, which took 0.046915 s (model generation: 0.046459, model checking: 0.000456): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : Yes: { r -> cons(_zegs_0, _zegs_1) ; y -> b } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_dfgs_0, _dfgs_1) ; _en -> s(s(_qhgs_0)) ; l -> cons(_ffgs_0, cons(_phgs_0, _phgs_1)) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> nil ; r -> cons(_yggs_0, nil) ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 12, which took 0.052120 s (model generation: 0.051602, model checking: 0.000518): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(nil) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_all(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : No: () eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> cons(_pjgs_0, _pjgs_1) ; x -> a ; y -> b } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> nil ; r -> cons(_pkgs_0, nil) ; y -> b } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 13, which took 0.100792 s (model generation: 0.100404, model checking: 0.000388): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(cons(x_0_0, x_0_1), b) <= True _r_2(nil, a) <= True _r_2(nil, b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(b, _rlgs_1) ; _en -> s(s(_oogs_0)) ; l -> cons(_tlgs_0, cons(_nogs_0, _nogs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> cons(_qngs_0, _qngs_1) ; x -> b ; y -> a } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(a, _xngs_1) ; r -> cons(_yngs_0, nil) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 14, which took 0.113790 s (model generation: 0.113215, model checking: 0.000575): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_3(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_3(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_fsgs_0)) ; l -> cons(b, cons(_esgs_0, _esgs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> s(z) ; r -> cons(b, nil) ; x -> b ; y -> a } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(_jrgs_0, _jrgs_1) ; r -> cons(b, _krgs_1) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 15, which took 0.140416 s (model generation: 0.139975, model checking: 0.000441): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(b, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(b, cons(a, nil)), nil) /\ delete_one(b, cons(b, cons(a, nil)), nil) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(nil) <= True _r_3(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_all(b, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_0) delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(b, _ksgs_1) ; _en -> s(s(_wvgs_0)) ; l -> cons(_msgs_0, cons(_vvgs_0, _vvgs_1)) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> cons(b, _rugs_1) ; x -> b ; y -> a } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(_bvgs_0, _bvgs_1) ; r -> cons(_cvgs_0, nil) ; y -> b } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 16, which took 0.162003 s (model generation: 0.161487, model checking: 0.000516): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) count(b, cons(b, cons(a, nil)), s(s(z))) <= count(b, cons(a, nil), s(z)) leqnat(s(z), s(z)) <= count(b, cons(a, nil), s(z)) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(b, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(b, cons(a, nil)), nil) /\ delete_one(b, cons(b, cons(a, nil)), nil) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_3(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True _r_3(b) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) /\ _r_3(x_1_0) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_twgs_0, _twgs_1) ; _en -> s(s(_jahs_0)) ; l -> cons(b, cons(_iahs_0, _iahs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(b, _zygs_1) ; r -> cons(b, _azgs_1) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> cons(_jzgs_0, _jzgs_1) ; r -> cons(b, _kzgs_1) ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 17, which took 0.451593 s (model generation: 0.449710, model checking: 0.001883): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(z) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_4(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_2(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_4(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) /\ _r_4(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(b) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(b, _cbhs_1) ; _en -> s(s(_ckhs_0)) ; l -> cons(b, cons(_qjhs_0, _qjhs_1)) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> s(z) ; r -> cons(b, _eehs_1) ; y -> b } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(b, _iihs_1) ; r -> cons(a, nil) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 18, which took 1.126781 s (model generation: 1.125685, model checking: 0.001096): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) /\ delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_5(x_0_0) _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_4(cons(x_0_0, x_0_1)) <= True _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(cons(x_0_0, x_0_1), a) <= True _r_2(nil, b) <= True _r_3(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1, x_2_0) delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : Yes: { r -> cons(b, _fkhs_1) ; y -> a } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_mrhs_0)) ; l -> cons(b, cons(b, _lrhs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> s(s(_orhs_0)) ; r -> cons(a, cons(b, _nrhs_1)) ; x -> b ; y -> a } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> s(z) ; r -> cons(a, cons(_rrhs_0, _rrhs_1)) ; y -> b } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> nil ; r -> cons(_nqhs_0, nil) ; x -> a ; y -> b } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 19, which took 0.935955 s (model generation: 0.934736, model checking: 0.001219): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) count(b, cons(a, cons(a, cons(b, nil))), s(s(z))) <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), nil) /\ delete_one(b, cons(b, cons(b, nil)), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(a, s(x_1_0)) <= True _r_2(a, z) <= True _r_2(b, z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_2(x_1_0, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_2(x_1_0, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_4(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_sshs_0, _sshs_1) ; _en -> s(s(_qxhs_0)) ; l -> cons(_ushs_0, cons(b, _pxhs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> s(s(_cyhs_0)) ; r -> cons(a, cons(_byhs_0, _byhs_1)) ; x -> a ; y -> b } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 20, which took 6.593204 s (model generation: 6.590576, model checking: 0.002628): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) count(b, cons(a, cons(a, cons(b, nil))), s(s(z))) <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, cons(b, nil)), s(s(z))) /\ delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), nil) /\ delete_one(b, cons(b, cons(b, nil)), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_2(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_lais_0, _lais_1) ; _en -> s(s(_klis_0)) ; l -> cons(b, cons(b, _vkis_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(_ekis_0, _ekis_1) ; r -> cons(a, cons(b, _ykis_1)) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 21, which took 1.942160 s (model generation: 1.939905, model checking: 0.002255): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) count(b, cons(a, cons(a, cons(b, nil))), s(s(z))) <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, cons(b, nil)), s(s(z))) /\ delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_all(b, cons(b, cons(b, nil)), nil) /\ delete_one(b, cons(b, cons(b, nil)), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(z) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_2(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_6(a) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : Yes: { r -> cons(b, nil) ; y -> b } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_pqis_0, cons(a, _jejs_1)) ; _en -> s(s(_qejs_0)) ; l -> cons(b, cons(b, _fejs_1)) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> s(s(_vdjs_0)) ; r -> cons(b, cons(b, _fejs_1)) ; x -> b ; y -> a } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : Yes: { _wm -> s(z) ; r -> cons(a, cons(b, _uejs_1)) ; y -> b } eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(b, _rbjs_1) ; r -> cons(a, cons(b, _kejs_1)) ; y -> a } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> cons(b, cons(a, _dejs_1)) ; r -> cons(b, nil) ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 22, which took 3.141720 s (model generation: 3.137775, model checking: 0.003945): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) count(b, cons(a, cons(a, cons(b, nil))), s(s(z))) <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, cons(b, nil)), s(s(z))) /\ delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_all(b, cons(b, cons(b, nil)), nil) /\ delete_one(b, cons(b, cons(b, nil)), nil) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_5(x_0_0) _r_1(cons(x_0_0, x_0_1), z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(nil, z) <= True _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_4(nil) <= True _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(cons(x_0_0, x_0_1), a) <= _r_6(x_0_0) _r_3(cons(x_0_0, x_0_1), b) <= _r_5(x_0_0) _r_3(nil, b) <= True _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_0) /\ _r_5(x_1_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_0) /\ _r_4(x_2_1) /\ _r_5(x_1_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1, x_2_0) /\ _r_4(x_2_1) /\ _r_6(x_1_0) /\ _r_6(x_2_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_6(x_1_0) delete_one(b, cons(x_1_0, x_1_1), nil) <= True delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : Yes: { r -> cons(b, cons(_vfks_0, _vfks_1)) ; y -> b } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(b, nil) ; _en -> s(s(_ahks_0)) ; l -> cons(b, nil) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> s(s(s(z))) ; r -> cons(a, cons(a, nil)) ; x -> a ; y -> b } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> nil ; r -> cons(b, nil) ; y -> b } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> nil ; r -> cons(b, _zrjs_1) ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 23, which took 12.374353 s (model generation: 12.372423, model checking: 0.001930): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) /\ delete_all(b, cons(b, nil), cons(b, nil)) /\ delete_one(b, cons(b, nil), cons(b, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) _r_2(cons(x_0_0, x_0_1), z) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(nil) <= True _r_5(a) <= True _r_6(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_6(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(nil) <= True _r_5(a) <= True _r_6(b) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_0) delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_2_0) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_ykks_0, _ykks_1) ; _en -> s(s(z)) ; l -> cons(a, cons(_ysks_0, cons(_xtks_0, _xtks_1))) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 24, which took 4.054131 s (model generation: 4.022022, model checking: 0.032109): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, cons(a, nil))), s(s(z))) /\ delete_all(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) /\ delete_all(b, cons(b, nil), cons(b, nil)) /\ delete_one(b, cons(b, nil), cons(b, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) /\ _r_4(x_0_1) _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) /\ _r_5(x_0_0) _r_1(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) /\ _r_6(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_5(a) <= True _r_6(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_2(x_1_1) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= _r_2(x_1_1) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= _r_2(x_1_1) count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) /\ _r_6(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_3(nil) <= True _r_5(a) <= True _r_6(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_6(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_6(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_2_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_5(x_2_0) delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) /\ _r_6(x_0_0) _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_3(nil) <= True _r_5(a) <= True _r_6(b) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_6(x_2_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_1_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_5(x_2_0) delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : Yes: { r -> cons(b, cons(b, _syns_1)) ; y -> a } leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> nil ; _en -> s(s(_izns_0)) ; l -> cons(b, nil) ; x -> b } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : Yes: { _xm -> z ; r -> cons(a, nil) ; x -> b ; y -> a } count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> cons(b, cons(b, _nbos_1)) ; x -> b ; y -> a } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(b, _cons_1) ; r -> cons(a, nil) ; y -> b } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> cons(a, _orns_1) ; r -> cons(a, nil) ; x -> a ; y -> b } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 25, which took 5.259602 s (model generation: 5.256572, model checking: 0.003030): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(z), s(s(z))) <= True leqnat(z, s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, cons(a, nil))), s(s(z))) /\ delete_all(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(b, cons(a, nil)), cons(b, nil)) <= delete_all(b, cons(a, nil), cons(b, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= delete_one(a, cons(a, nil), cons(a, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) leqnat(s(s(z)), s(s(z))) <= leqnat(s(z), s(z)) leqnat(z, z) <= leqnat(s(z), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_2_0) delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_5(x_2_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(b, _lrqs_1) ; _en -> s(z) ; l -> cons(b, cons(_ujrs_0, _ujrs_1)) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> cons(b, _lcrs_1) ; r -> cons(a, nil) ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 26, which took 11.494401 s (model generation: 11.490495, model checking: 0.003906): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(s(z)), s(s(z))) <= True leqnat(s(z), s(s(z))) <= True leqnat(s(z), s(z)) <= True leqnat(z, s(z)) <= True leqnat(z, z) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, cons(a, nil))), s(s(z))) /\ delete_all(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(b, cons(a, nil)), cons(b, nil)) <= delete_all(b, cons(a, nil), cons(b, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= delete_one(a, cons(a, nil), cons(a, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= delete_one(b, cons(a, nil), cons(b, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_1(x_0_1, x_1_0) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_2(x_0_1, x_1_0) _r_2(cons(x_0_0, x_0_1), z) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_5(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_5(x_2_0) delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, cons(x_1_0, x_1_1), nil) <= _r_5(x_1_0) delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_3(nil) <= True _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_5(x_2_0) delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_2_0) delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_4(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_5(x_1_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_6(x_1_0) /\ _r_6(x_2_0) delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ _r_5(x_2_0) delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_3(x_1_1) /\ _r_5(x_1_0) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(b, _yprs_1) ; _en -> s(s(z)) ; l -> cons(b, cons(_ekss_0, cons(_flss_0, _flss_1))) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : No: () delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : No: () eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : Yes: { _lm -> cons(a, _tbss_1) ; r -> cons(a, nil) ; x -> b ; y -> a } leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () ------------------------------------------- Step 27, which took 7.639643 s (model generation: 7.624710, model checking: 0.014933): Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(s(z)), s(s(z))) <= True leqnat(s(z), s(s(z))) <= True leqnat(s(z), s(z)) <= True leqnat(z, s(z)) <= True leqnat(z, z) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, cons(a, nil))), s(s(z))) /\ delete_all(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) False <= delete_all(a, cons(b, cons(a, cons(a, nil))), cons(b, nil)) /\ delete_one(a, cons(b, cons(a, cons(a, nil))), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(b, cons(b, cons(a, nil)), cons(b, nil)) <= delete_all(b, cons(a, nil), cons(b, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= delete_one(a, cons(a, nil), cons(a, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= delete_one(b, cons(a, nil), cons(b, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(a) <= True _r_6(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(a) <= True _r_6(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_6(x_1_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () delete_all(x, nil, nil) <= True : No: () delete_one(x, nil, nil) <= True : No: () delete_one(y, cons(y, r), r) <= True : No: () leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) : Yes: { _dn -> cons(_epss_0, _epss_1) ; _en -> s(s(_wyts_0)) ; l -> cons(a, cons(b, cons(_iyts_0, cons(a, nil)))) ; x -> a } eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) : No: () count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) : No: () eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) : Yes: { _rm -> nil ; r -> cons(b, _bfts_1) ; x -> a ; y -> b } delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) : Yes: { _qm -> cons(_zwts_0, _zwts_1) ; r -> cons(b, cons(a, nil)) ; y -> b } eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) : No: () leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) : No: () leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) : No: () False <= leqnat(s(nn1), z) : No: () Total time: 59.907152 Learner time: 55.807415 Teacher time: 0.074939 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { count(x, nil, z) <= True -> 0 delete_all(x, nil, nil) <= True -> 0 delete_one(x, nil, nil) <= True -> 0 delete_one(y, cons(y, r), r) <= True -> 0 leqnat(_en, s(z)) <= count(x, l, _en) /\ delete_all(x, l, _dn) /\ delete_one(x, l, _dn) -> 0 eq_elt(x, y) \/ count(x, cons(y, r), _xm) <= count(x, r, _xm) -> 0 count(y, cons(y, r), s(_wm)) <= count(y, r, _wm) -> 0 eq_elt(x, y) \/ delete_all(x, cons(y, r), cons(y, _rm)) <= delete_all(x, r, _rm) -> 0 delete_all(y, cons(y, r), _qm) <= delete_all(y, r, _qm) -> 0 eq_elt(x, y) \/ delete_one(x, cons(y, r), cons(y, _lm)) <= delete_one(x, r, _lm) -> 0 leqnat(s(nn1), s(nn2)) <= leqnat(nn1, nn2) -> 0 leqnat(nn1, nn2) <= leqnat(s(nn1), s(nn2)) -> 0 False <= leqnat(s(nn1), z) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(z))) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, cons(b, nil))), s(s(z))) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, cons(b, nil)), s(s(z))) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True delete_all(a, cons(a, cons(a, cons(b, nil))), cons(b, nil)) <= True delete_all(a, cons(a, cons(a, nil)), nil) <= True delete_all(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_all(a, cons(a, nil), nil) <= True delete_all(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_all(a, cons(b, nil), cons(b, nil)) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= True delete_all(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_all(b, cons(a, nil), cons(a, nil)) <= True delete_all(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, cons(a, nil))), cons(a, nil)) <= True delete_all(b, cons(b, cons(b, nil)), nil) <= True delete_all(b, cons(b, nil), nil) <= True delete_all(b, nil, nil) <= True delete_one(a, cons(a, cons(a, nil)), cons(a, nil)) <= True delete_one(a, cons(a, cons(b, cons(b, nil))), cons(b, cons(b, nil))) <= True delete_one(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete_one(a, cons(a, nil), nil) <= True delete_one(a, cons(b, cons(a, nil)), cons(b, nil)) <= True delete_one(a, cons(b, nil), cons(b, nil)) <= True delete_one(a, nil, nil) <= True delete_one(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete_one(b, cons(a, cons(b, nil)), cons(a, nil)) <= True delete_one(b, cons(a, nil), cons(a, nil)) <= True delete_one(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete_one(b, cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= True delete_one(b, cons(b, cons(b, nil)), cons(b, nil)) <= True delete_one(b, cons(b, nil), nil) <= True delete_one(b, nil, nil) <= True leqnat(s(s(z)), s(s(z))) <= True leqnat(s(z), s(s(z))) <= True leqnat(s(z), s(z)) <= True leqnat(z, s(z)) <= True leqnat(z, z) <= True count(a, cons(b, cons(a, cons(a, nil))), s(s(s(z)))) <= count(a, cons(a, cons(a, nil)), s(s(s(z)))) False <= count(a, cons(a, cons(b, cons(a, cons(a, nil)))), s(s(z))) /\ delete_all(a, cons(a, cons(b, cons(a, cons(a, nil)))), cons(a, nil)) /\ delete_one(a, cons(a, cons(b, cons(a, cons(a, nil)))), cons(a, nil)) False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(a, cons(a, cons(a, nil))), s(s(z))) /\ delete_all(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, cons(a, nil))), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(b, cons(a, cons(a, nil)), cons(b, nil)) False <= count(b, cons(a, cons(a, nil)), s(s(z))) /\ delete_all(b, cons(a, cons(a, nil)), nil) /\ delete_one(b, cons(a, cons(a, nil)), nil) count(b, cons(b, cons(a, cons(a, nil))), s(s(z))) <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(s(z))) /\ delete_all(b, cons(a, nil), nil) /\ delete_one(b, cons(a, nil), nil) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, nil), s(s(z))) False <= delete_all(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) /\ delete_one(a, cons(a, cons(a, nil)), cons(b, nil)) delete_all(a, cons(a, cons(a, cons(b, nil))), cons(a, nil)) <= delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete_all(a, cons(a, nil), cons(a, nil)) delete_all(a, cons(a, cons(a, nil)), cons(b, nil)) <= delete_all(a, cons(a, nil), cons(b, nil)) False <= delete_all(a, cons(b, cons(a, cons(a, nil))), cons(b, nil)) /\ delete_one(a, cons(b, cons(a, cons(a, nil))), cons(b, nil)) delete_all(a, cons(a, cons(b, nil)), cons(a, nil)) <= delete_all(a, cons(b, nil), cons(a, nil)) delete_all(a, cons(b, cons(b, nil)), cons(b, nil)) <= delete_all(a, cons(b, nil), nil) delete_all(b, cons(b, cons(a, nil)), cons(b, nil)) <= delete_all(b, cons(a, nil), cons(b, nil)) delete_all(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_all(b, cons(a, nil), nil) delete_all(b, cons(b, cons(a, nil)), nil) <= delete_all(b, cons(a, nil), nil) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, cons(a, nil))) False <= delete_all(b, cons(b, cons(b, nil)), cons(a, nil)) /\ delete_one(b, cons(b, cons(b, nil)), cons(a, nil)) False <= delete_one(a, cons(a, cons(a, nil)), nil) delete_one(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= delete_one(a, cons(a, nil), cons(a, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) <= delete_one(b, cons(a, nil), cons(b, nil)) delete_one(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete_one(b, cons(a, nil), nil) False <= delete_one(b, cons(b, cons(b, nil)), nil) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete_one(b, cons(b, nil), cons(a, nil)) delete_one(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(a, nil)))) <= delete_one(b, cons(b, nil), cons(b, cons(a, nil))) False <= leqnat(s(s(z)), s(z)) False <= leqnat(s(z), z) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= _r_4(x_0_1) _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(a) <= True _r_6(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_1) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_1) /\ _r_6(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; delete_all -> [ delete_all : { _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_4(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _r_4(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(a) <= True _r_6(b) <= True delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_6(x_1_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_all(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(a, cons(x_1_0, x_1_1), nil) <= True delete_all(a, nil, nil) <= True delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) delete_all(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_1) /\ _r_5(x_1_0) delete_all(b, cons(x_1_0, x_1_1), nil) <= True delete_all(b, nil, nil) <= True } ] ; delete_one -> [ delete_one : { _r_2(nil) <= True delete_one(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(a, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(a, nil, nil) <= True delete_one(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete_one(b, cons(x_1_0, x_1_1), nil) <= _r_2(x_1_1) delete_one(b, nil, nil) <= True } ] ; leqnat -> [ leqnat : { leqnat(s(x_0_0), s(x_1_0)) <= leqnat(x_0_0, x_1_0) leqnat(z, s(x_1_0)) <= True leqnat(z, z) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _|