Solving ../../benchmarks/smtlib/true/timbuk_delete_not_member.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: Some(60.) (sec) Teacher_type: Checks all clauses every time Approximation method: remove every clause that can be safely removed Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} } definition: { (delete, F: { delete(x, nil, nil) <= True delete(h, cons(h, t), _aia) <= delete(h, t, _aia) eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) } eq_eltlist(_eia, _fia) <= delete(_cia, _dia, _eia) /\ delete(_cia, _dia, _fia) ) (mem, P: { mem(h, cons(h, t)) <= True eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) False <= mem(e, nil) } ) } properties: { False <= delete(i, l, _gia) /\ mem(i, _gia) } over-approximation: {delete, mem} under-approximation: {} Clause system for inference is: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Solving took 60.173665 seconds. Maybe: timeout during learnerLast solver state: Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= delete(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, cons(b, nil)))), cons(b, cons(b, nil))) <= delete(a, cons(b, cons(b, cons(b, nil))), cons(b, cons(b, nil))) False <= delete(a, cons(b, cons(b, nil)), cons(a, cons(b, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) delete(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= delete(b, cons(a, nil), cons(a, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) False <= delete(b, cons(b, nil), cons(a, cons(b, nil))) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _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_4(nil) <= True _r_5(b) <= True _r_6(a) <= True delete(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_5(x_1_0) /\ _r_5(x_2_0) /\ mem(x_1_0, x_2_1) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_2_0) /\ mem(x_1_0, x_2_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_6(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _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 _r_6(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005646 s (model generation: 0.005598, model checking: 0.000048): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None delete -> [ delete : { } ] ; mem -> [ mem : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : Yes: { x -> b } mem(h, cons(h, t)) <= True : Yes: { h -> b } delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : No: () eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 1, which took 0.006217 s (model generation: 0.006135, model checking: 0.000082): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(b, nil, nil) <= True mem(b, cons(b, nil)) <= True } Current best model: |_ name: None delete -> [ delete : { delete(b, nil, nil) <= True } ] ; mem -> [ mem : { mem(b, cons(x_1_0, x_1_1)) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : Yes: { x -> a } mem(h, cons(h, t)) <= True : Yes: { h -> a } delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> nil ; h -> b ; t -> nil } False <= delete(i, l, _gia) /\ mem(i, _gia) : No: () eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> nil ; h -> a ; t -> nil ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> b ; h -> a ; t -> nil } ------------------------------------------- Step 2, which took 0.015366 s (model generation: 0.012460, model checking: 0.002906): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(b, cons(b, nil)) <= True mem(b, nil) <= mem(b, cons(a, nil)) } Current best model: |_ name: None delete -> [ delete : { delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { mem(a, cons(x_1_0, x_1_1)) <= True mem(b, cons(x_1_0, x_1_1)) <= True mem(b, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> nil ; h -> a ; t -> nil } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> nil ; i -> b ; l -> nil } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> nil ; h -> b ; t -> nil ; x -> a } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> a ; h -> b ; t -> nil } ------------------------------------------- Step 3, which took 0.020270 s (model generation: 0.020074, model checking: 0.000196): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(b, cons(b, nil)) <= True mem(a, nil) <= mem(a, cons(b, nil)) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(b) <= True mem(a, cons(x_1_0, x_1_1)) <= True mem(a, nil) <= True mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> nil ; i -> a ; l -> nil } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> b ; h -> a ; t -> cons(b, _cnnad_1) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 4, which took 0.036005 s (model generation: 0.035766, model checking: 0.000239): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(a) <= True _r_3(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(_qnnad_0, cons(_yonad_0, _yonad_1)) ; i -> b ; l -> cons(_snnad_0, _snnad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> a ; h -> b ; t -> cons(a, _ynnad_1) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> b ; h -> a ; t -> cons(a, nil) } ------------------------------------------- Step 5, which took 0.042382 s (model generation: 0.041721, model checking: 0.000661): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(_gpnad_0, cons(_drnad_0, _drnad_1)) ; i -> a ; l -> cons(_ipnad_0, _ipnad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> b ; h -> a ; t -> cons(a, cons(b, _hrnad_1)) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> a ; h -> b ; t -> cons(b, nil) } ------------------------------------------- Step 6, which took 0.051422 s (model generation: 0.050628, model checking: 0.000794): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_4(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(_trnad_0, _trnad_1) ; h -> a ; t -> cons(b, _vrnad_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, _zrnad_1) ; i -> a ; l -> cons(b, _bsnad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> a ; h -> b ; t -> cons(b, cons(a, _ounad_1)) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 7, which took 0.062780 s (model generation: 0.061983, model checking: 0.000797): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_4(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, _rvnad_1) ; i -> b ; l -> cons(_tvnad_0, _tvnad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 8, which took 0.063356 s (model generation: 0.062400, model checking: 0.000956): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, nil), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_3(b) <= True _r_4(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _ecoad_1)) ; i -> a ; l -> cons(_hznad_0, _hznad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 9, which took 0.065100 s (model generation: 0.064177, model checking: 0.000923): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, nil), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_3(b) <= True _r_4(a) <= True delete(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(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(b) <= True _r_4(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, _kdoad_1) ; h -> a ; t -> cons(b, _mdoad_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, _ehoad_1)) ; i -> b ; l -> cons(_beoad_0, _beoad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 10, which took 0.128907 s (model generation: 0.127884, model checking: 0.001023): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_2(nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : No: () eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(a, nil) ; h -> a ; t -> cons(_ikoad_0, _ikoad_1) ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 11, which took 0.191152 s (model generation: 0.190295, model checking: 0.000857): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, _btoad_1)) ; i -> b ; l -> cons(_rooad_0, cons(_atoad_0, _atoad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 12, which took 0.197895 s (model generation: 0.196388, model checking: 0.001507): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _azoad_1)) ; i -> b ; l -> cons(_bvoad_0, _bvoad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(b, nil) ; h -> b ; t -> cons(_kvoad_0, _kvoad_1) ; x -> a } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 13, which took 0.280225 s (model generation: 0.278514, model checking: 0.001711): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _jipad_1)) ; i -> b ; l -> cons(_xcpad_0, cons(a, _jipad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(a, nil) ; h -> a ; t -> cons(b, nil) ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 14, which took 0.402412 s (model generation: 0.400504, model checking: 0.001908): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, _fmpad_1) ; i -> a ; l -> cons(_hmpad_0, cons(a, _dspad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(b, nil) ; h -> b ; t -> cons(b, nil) ; x -> a } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 15, which took 0.497586 s (model generation: 0.495861, model checking: 0.001725): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) delete(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(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, cons(_sdqad_0, _sdqad_1)) ; h -> a ; t -> cons(b, _vupad_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _odqad_1)) ; i -> a ; l -> cons(b, _lwpad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 16, which took 0.511838 s (model generation: 0.509162, model checking: 0.002676): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(a, nil) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) /\ mem(x_1_0, x_2_1) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ mem(x_1_0, x_2_1) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(a, cons(b, _lqqad_1)) ; h -> a ; t -> cons(b, _rgqad_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, _lqqad_1)) ; i -> a ; l -> cons(b, _hiqad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 17, which took 0.534498 s (model generation: 0.531525, model checking: 0.002973): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(a, nil) <= True _r_1(b, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_5(x_2_0) delete(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) /\ mem(x_1_0, x_2_1) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) /\ mem(x_1_0, x_2_1) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, cons(b, _ilrad_1)) ; h -> a ; t -> cons(b, _dvqad_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(a, cons(b, _xjrad_1))) ; i -> b ; l -> cons(a, _ayqad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 18, which took 0.624861 s (model generation: 0.623840, model checking: 0.001021): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(nil, nil) <= 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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(a, nil) ; h -> b ; t -> cons(_iorad_0, nil) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, _vorad_1) ; i -> a ; l -> cons(_xorad_0, cons(b, _utrad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> nil ; h -> a ; t -> cons(_grrad_0, _grrad_1) ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 19, which took 0.797263 s (model generation: 0.792558, model checking: 0.004705): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, _ryrad_1) ; i -> b ; l -> cons(_tyrad_0, cons(b, _vhsad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 20, which took 0.780316 s (model generation: 0.777237, model checking: 0.003079): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _zusad_1)) ; i -> a ; l -> cons(_bosad_0, cons(b, _wusad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 21, which took 0.808229 s (model generation: 0.801966, model checking: 0.006263): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_1(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_2(x_1_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _nrtad_1)) ; i -> b ; l -> cons(_vetad_0, cons(b, _prtad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 22, which took 0.885598 s (model generation: 0.878841, model checking: 0.006757): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(nil) <= True _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_2(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, cons(a, _ppuad_1))) ; i -> b ; l -> cons(_ubuad_0, cons(a, _ppuad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 23, which took 0.735638 s (model generation: 0.732481, model checking: 0.003157): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) /\ mem(b, cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= 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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, cons(a, nil)) ; h -> a ; t -> cons(b, cons(a, _uhvad_1)) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, _udvad_1)) ; i -> b ; l -> cons(_uwuad_0, cons(b, _rdvad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 24, which took 1.109710 s (model generation: 1.101362, model checking: 0.008348): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) /\ mem(b, cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(nil) <= 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_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1) /\ _r_3(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) _r_2(nil) <= 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_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(a, cons(b, nil))) ; i -> b ; l -> cons(_vsvad_0, cons(b, nil)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : Yes: { e -> b ; h -> a ; t -> cons(b, cons(a, nil)) } eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 25, which took 1.086638 s (model generation: 1.081850, model checking: 0.004788): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) /\ mem(b, cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) mem(b, cons(a, cons(b, cons(a, nil)))) <= mem(b, cons(b, cons(a, nil))) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_5(x_2_0) delete(a, 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(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(a, _qswad_1) ; h -> a ; t -> cons(b, cons(b, _sixad_1)) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _uixad_1)) ; i -> a ; l -> cons(_xuwad_0, cons(a, _qixad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(a, nil) ; h -> a ; t -> cons(b, cons(a, _ioxad_1)) ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 26, which took 1.282833 s (model generation: 1.279796, model checking: 0.003037): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) /\ mem(a, cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) /\ mem(b, cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) mem(b, cons(a, cons(b, cons(a, nil)))) <= mem(b, cons(b, cons(a, nil))) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_2(nil) <= 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_4(x_0_0) _r_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= mem(x_1_0, x_2_1) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) _r_2(nil) <= 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_4(x_0_0) _r_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : Yes: { h -> a ; t -> cons(b, nil) } delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, cons(a, nil)) ; h -> b ; t -> cons(a, _ypxad_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(_cqxad_0, cons(a, cons(b, nil))) ; i -> a ; l -> cons(_eqxad_0, _eqxad_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(b, cons(b, nil)) ; h -> a ; t -> cons(b, _nsxad_1) ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : Yes: { e -> a ; h -> b ; t -> cons(a, cons(b, nil)) } ------------------------------------------- Step 27, which took 1.812752 s (model generation: 1.807424, model checking: 0.005328): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) /\ mem(b, cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) delete(b, cons(b, cons(a, nil)), cons(b, cons(a, nil))) <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) /\ mem(b, cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) mem(b, cons(a, cons(b, cons(a, nil)))) <= mem(b, cons(b, cons(a, nil))) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_2(x_1_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(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(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_1(nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) /\ _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : Yes: { h -> b ; t -> cons(a, nil) } delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, nil) ; i -> b ; l -> cons(_riyad_0, cons(a, _iwyad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(b, nil) ; h -> a ; t -> cons(_xoyad_0, cons(a, _iwyad_1)) ; x -> b } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 28, which took 1.686148 s (model generation: 1.678466, model checking: 0.007682): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, cons(_zcabd_0, _zcabd_1)) ; h -> a ; t -> cons(b, cons(b, nil)) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, _qwzad_1)) ; i -> a ; l -> cons(b, cons(b, _owzad_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 29, which took 1.640274 s (model generation: 1.626414, model checking: 0.013860): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, cons(b, _qsbbd_1))) ; i -> a ; l -> cons(_rzabd_0, _rzabd_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 30, which took 1.664310 s (model generation: 1.651848, model checking: 0.012462): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(a) <= True _r_5(b) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, _bcebd_1)) ; i -> a ; l -> cons(_zjdbd_0, cons(b, _bcebd_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 31, which took 1.734444 s (model generation: 1.718790, model checking: 0.015654): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_1) /\ _r_3(x_2_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : No: () False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, cons(b, _qmgbd_1))) ; i -> a ; l -> cons(_jrfbd_0, cons(b, _qmgbd_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 32, which took 1.620356 s (model generation: 1.609839, model checking: 0.010517): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(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_4(x_1_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(a, cons(b, _udjbd_1)) ; h -> a ; t -> cons(b, cons(b, _udjbd_1)) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, _udjbd_1)) ; i -> a ; l -> cons(b, cons(b, _udjbd_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 33, which took 1.635056 s (model generation: 1.621049, model checking: 0.014007): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, cons(b, nil)), cons(a, cons(b, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1) _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) _r_1(cons(x_0_0, x_0_1), nil) <= True _r_1(nil, nil) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(b) <= True _r_5(a) <= True delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_2(x_1_1) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) delete(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_4(x_1_0) /\ _r_4(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_3(x_1_1) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_1) /\ _r_5(x_1_0) /\ _r_5(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True } ] ; mem -> [ mem : { _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(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_4(b) <= True _r_5(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(b, cons(b, _yfmbd_1)) ; h -> a ; t -> cons(b, cons(b, cons(b, nil))) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(b, cons(a, cons(b, _mllbd_1))) ; i -> a ; l -> cons(b, cons(b, _mllbd_1)) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : No: () eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () ------------------------------------------- Step 34, which took 36.137846 s (model generation: 36.133895, model checking: 0.003951): Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, cons(b, nil)))), cons(b, cons(b, nil))) <= delete(a, cons(b, cons(b, cons(b, nil))), cons(b, cons(b, nil))) False <= delete(a, cons(b, cons(b, nil)), cons(a, cons(b, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _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_4(nil) <= True _r_5(b) <= True _r_6(a) <= True delete(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_5(x_1_0) /\ _r_5(x_2_0) /\ mem(x_1_0, x_2_1) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_2_0) /\ mem(x_1_0, x_2_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_6(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _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 _r_6(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: delete(x, nil, nil) <= True : No: () mem(h, cons(h, t)) <= True : No: () delete(h, cons(h, t), _aia) <= delete(h, t, _aia) : Yes: { _aia -> cons(a, cons(a, nil)) ; h -> b ; t -> cons(a, _aanbd_1) } False <= delete(i, l, _gia) /\ mem(i, _gia) : Yes: { _gia -> cons(a, cons(b, nil)) ; i -> b ; l -> cons(b, _nbnbd_1) } eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) : Yes: { _bia -> cons(b, nil) ; h -> b ; t -> cons(_ndnbd_0, cons(_jpnbd_0, _jpnbd_1)) ; x -> a } eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) : No: () eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) : No: () Total time: 60.173665 Learner time: 59.008730 Teacher time: 0.146599 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { delete(x, nil, nil) <= True -> 0 mem(h, cons(h, t)) <= True -> 0 delete(h, cons(h, t), _aia) <= delete(h, t, _aia) -> 0 False <= delete(i, l, _gia) /\ mem(i, _gia) -> 0 eq_elt(x, h) \/ delete(x, cons(h, t), cons(h, _bia)) <= delete(x, t, _bia) -> 0 eq_elt(e, h) \/ mem(e, cons(h, t)) <= mem(e, t) -> 0 eq_elt(e, h) \/ mem(e, t) <= mem(e, cons(h, t)) -> 0 } Accumulated learning constraints: { delete(a, cons(a, cons(b, nil)), cons(b, nil)) <= True delete(a, cons(a, nil), nil) <= True delete(a, cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True delete(a, cons(b, nil), cons(b, nil)) <= True delete(a, nil, nil) <= True delete(b, cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True delete(b, cons(a, cons(b, cons(a, nil))), cons(a, cons(a, nil))) <= True delete(b, cons(a, nil), cons(a, nil)) <= True delete(b, cons(b, cons(a, nil)), cons(a, nil)) <= True delete(b, cons(b, nil), nil) <= True delete(b, nil, nil) <= True mem(a, cons(a, cons(b, nil))) <= True mem(a, cons(a, nil)) <= True mem(a, cons(b, cons(a, nil))) <= True mem(a, cons(b, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(a, cons(b, nil)))) <= True mem(b, cons(a, cons(b, cons(a, nil)))) <= True mem(b, cons(a, cons(b, nil))) <= True mem(b, cons(b, cons(a, nil))) <= True mem(b, cons(b, nil)) <= True False <= delete(a, cons(a, cons(a, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, cons(a, nil))), cons(b, cons(b, nil))) <= delete(a, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(a, cons(a, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(a, nil), cons(a, cons(a, cons(b, nil)))) /\ mem(a, cons(a, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(a, cons(a, nil))) /\ mem(a, cons(a, cons(a, nil))) False <= delete(a, cons(a, nil), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(a, nil), cons(b, cons(a, nil))) delete(a, cons(b, cons(a, nil)), cons(b, cons(b, nil))) <= delete(a, cons(a, nil), cons(b, nil)) delete(a, cons(a, cons(b, cons(a, nil))), cons(b, cons(a, nil))) <= delete(a, cons(b, cons(a, nil)), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, cons(b, cons(b, nil)))), cons(b, cons(b, nil))) <= delete(a, cons(b, cons(b, cons(b, nil))), cons(b, cons(b, nil))) False <= delete(a, cons(b, cons(b, nil)), cons(a, cons(b, nil))) delete(a, cons(a, cons(b, cons(b, nil))), cons(a, nil)) <= delete(a, cons(b, cons(b, nil)), cons(a, nil)) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, cons(b, nil)))) /\ mem(a, cons(b, cons(a, cons(b, nil)))) False <= delete(a, cons(b, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(a, cons(b, nil), cons(a, cons(b, nil))) False <= delete(a, cons(b, nil), cons(a, nil)) False <= delete(a, cons(b, nil), cons(b, cons(a, nil))) delete(a, cons(a, cons(b, nil)), cons(b, cons(b, nil))) <= delete(a, cons(b, nil), cons(b, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, cons(a, nil)))) False <= delete(b, cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(a, nil)), cons(b, nil)) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(a, cons(b, nil)))) False <= delete(b, cons(a, cons(b, nil)), cons(a, cons(b, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, cons(a, nil))) False <= delete(b, cons(a, cons(b, nil)), cons(b, nil)) False <= delete(b, cons(a, nil), cons(a, cons(a, cons(b, nil)))) delete(b, cons(b, cons(a, nil)), cons(a, cons(a, nil))) <= delete(b, cons(a, nil), cons(a, cons(a, nil))) False <= delete(b, cons(a, nil), cons(a, cons(b, nil))) False <= delete(b, cons(a, nil), cons(b, cons(a, nil))) False <= delete(b, cons(a, nil), cons(b, nil)) delete(b, cons(a, cons(a, nil)), cons(a, nil)) <= delete(b, cons(a, nil), nil) False <= delete(b, cons(b, nil), cons(a, cons(b, nil))) delete(b, cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= delete(b, cons(b, nil), cons(a, nil)) delete(b, cons(a, cons(b, nil)), cons(a, cons(b, cons(b, nil)))) <= delete(b, cons(b, nil), cons(b, cons(b, nil))) False <= mem(a, cons(b, cons(b, nil))) False <= mem(a, cons(b, nil)) False <= mem(a, nil) False <= mem(b, cons(a, cons(a, nil))) False <= mem(b, cons(a, nil)) False <= mem(b, nil) } Current best model: |_ name: None delete -> [ delete : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_1) _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_4(nil) <= True _r_5(b) <= True _r_6(a) <= True delete(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_5(x_1_0) /\ _r_5(x_2_0) /\ mem(x_1_0, x_2_1) delete(a, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_5(x_2_0) delete(a, cons(x_1_0, x_1_1), nil) <= True delete(a, nil, nil) <= True delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) /\ _r_6(x_2_0) /\ mem(x_1_0, x_2_1) delete(b, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_1) /\ _r_6(x_2_0) delete(b, cons(x_1_0, x_1_1), nil) <= True delete(b, nil, nil) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; mem -> [ mem : { _r_1(cons(x_0_0, x_0_1)) <= _r_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _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 _r_6(a) <= True mem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) mem(a, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) mem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) mem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _|