Solving ../../benchmarks/smtlib/true/isaplanner_prop26.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: { (elem, P: { elem(h1, cons(h1, t1)) <= True eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) False <= elem(e, nil) } ) (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) } eq_eltlist(_ha, _ia) <= append(_fa, _ga, _ha) /\ append(_fa, _ga, _ia) ) } properties: { elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) } over-approximation: {append} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Solving took 60.733792 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(b, nil))) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, cons(a, nil))), nil, cons(a, nil)) /\ elem(b, cons(a, cons(b, cons(a, nil)))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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_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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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(a) <= True _r_5(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(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.006166 s (model generation: 0.006111, model checking: 0.000055): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; elem -> [ elem : { } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } elem(h1, cons(h1, t1)) <= True : Yes: { h1 -> b } elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : No: () append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 1, which took 0.006285 s (model generation: 0.006182, model checking: 0.000103): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True elem(b, cons(b, nil)) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; elem -> [ elem : { elem(b, cons(x_1_0, x_1_1)) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_tqaf_0, _tqaf_1) } elem(h1, cons(h1, t1)) <= True : Yes: { h1 -> a } elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : No: () append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> nil ; l2 -> nil ; t1 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : Yes: { e -> b ; h1 -> a ; t1 -> nil } False <= elem(e, nil) : No: () ------------------------------------------- Step 2, which took 0.008433 s (model generation: 0.008173, model checking: 0.000260): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(b, cons(b, nil)) <= True elem(b, nil) <= elem(b, cons(a, nil)) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { elem(a, cons(x_1_0, x_1_1)) <= True elem(b, cons(x_1_0, x_1_1)) <= True elem(b, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : No: () append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(_braf_0, _braf_1) ; l2 -> cons(_craf_0, _craf_1) ; t1 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : Yes: { e -> a ; h1 -> b ; t1 -> nil } False <= elem(e, nil) : Yes: { e -> b } ------------------------------------------- Step 3, which took 0.016472 s (model generation: 0.016317, model checking: 0.000155): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(b, cons(b, nil)) <= True elem(a, nil) <= elem(a, cons(b, nil)) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _r_1(b) <= True elem(a, cons(x_1_0, x_1_1)) <= True elem(a, nil) <= True elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, _nraf_1) ; i -> b ; l1 -> cons(b, _praf_1) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : Yes: { e -> b ; h1 -> a ; t1 -> cons(b, _traf_1) } eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : Yes: { e -> a } ------------------------------------------- Step 4, which took 0.048284 s (model generation: 0.047864, model checking: 0.000420): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(b, nil), nil, cons(a, nil)) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_2(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(a) <= True _r_3(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, _fsaf_1) ; i -> a ; l1 -> cons(a, _hsaf_1) ; l2 -> cons(_isaf_0, _isaf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> nil ; h1 -> b ; l2 -> nil ; t1 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : Yes: { e -> a ; h1 -> b ; t1 -> cons(a, _ltaf_1) } eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : Yes: { e -> b ; h1 -> a ; t1 -> cons(a, nil) } False <= elem(e, nil) : No: () ------------------------------------------- Step 5, which took 0.090449 s (model generation: 0.089853, model checking: 0.000596): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_3(a) <= True _r_4(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, nil) ; i -> a ; l1 -> cons(a, cons(_ryaf_0, _ryaf_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(a, _rwaf_1) ; h1 -> b ; l2 -> cons(_swaf_0, _swaf_1) ; t1 -> cons(_twaf_0, _twaf_1) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : Yes: { e -> b ; h1 -> a ; t1 -> cons(a, cons(b, _zyaf_1)) } eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : Yes: { e -> a ; h1 -> b ; t1 -> cons(b, nil) } False <= elem(e, nil) : No: () ------------------------------------------- Step 6, which took 0.214825 s (model generation: 0.214000, model checking: 0.000825): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, nil) ; i -> a ; l1 -> cons(b, cons(a, _ffbf_1)) ; l2 -> cons(_eabf_0, _eabf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : Yes: { e -> a ; h1 -> b ; t1 -> cons(b, cons(a, _pfbf_1)) } eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 7, which took 0.236892 s (model generation: 0.235955, model checking: 0.000937): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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_3(a) <= True _r_4(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, nil) ; i -> a ; l1 -> cons(b, cons(a, _elbf_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(b, nil) ; l2 -> cons(_djbf_0, _djbf_1) ; t1 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 8, which took 0.605100 s (model generation: 0.604114, model checking: 0.000986): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(nil, b) <= 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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, nil) ; i -> a ; l1 -> cons(a, nil) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(b, nil) ; h1 -> b ; l2 -> cons(_npbf_0, _npbf_1) ; t1 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 9, which took 0.732883 s (model generation: 0.731616, model checking: 0.001267): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_4(b) <= True _r_5(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, nil) ; i -> b ; l1 -> cons(a, cons(b, _yacf_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 10, which took 0.716913 s (model generation: 0.715424, model checking: 0.001489): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_4(a) <= True _r_5(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, nil) ; i -> b ; l1 -> cons(b, nil) ; l2 -> cons(_wdcf_0, _wdcf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 11, which took 0.831096 s (model generation: 0.829552, model checking: 0.001544): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_4(b) <= True _r_5(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, cons(b, nil)) ; i -> a ; l1 -> cons(b, cons(a, _lzcf_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 12, which took 0.769678 s (model generation: 0.768330, model checking: 0.001348): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(b, _qzcf_1) } elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, cons(a, nil)) ; i -> b ; l1 -> cons(b, _hadf_1) ; l2 -> cons(_iadf_0, _iadf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(a, _zcdf_1) ; h1 -> a ; l2 -> nil ; t1 -> cons(a, nil) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 13, which took 0.876714 s (model generation: 0.875130, model checking: 0.001584): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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(a) <= True _r_5(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, cons(a, nil)) ; i -> b ; l1 -> cons(b, _xkdf_1) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(a, _lldf_1) ; h1 -> b ; l2 -> cons(_mldf_0, _mldf_1) ; t1 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 14, which took 1.125150 s (model generation: 1.123556, model checking: 0.001594): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_1_0) _r_1(nil, cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_4(b) <= True _r_5(a) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, nil) ; i -> b ; l1 -> cons(a, cons(b, _hcef_1)) ; l2 -> cons(_eudf_0, _eudf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(b, nil) ; h1 -> b ; l2 -> cons(_zvdf_0, _zvdf_1) ; t1 -> cons(b, nil) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 15, which took 1.625771 s (model generation: 1.623453, model checking: 0.002318): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, cons(a, nil)) ; i -> b ; l1 -> cons(a, cons(b, _cuef_1)) ; l2 -> cons(_pgef_0, _pgef_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(_ykef_0, cons(a, _xtef_1)) ; h1 -> b ; l2 -> nil ; t1 -> cons(a, _alef_1) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 16, which took 2.014335 s (model generation: 2.010788, model checking: 0.003547): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_1_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_2_0) append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, cons(a, nil)) ; i -> b ; l1 -> cons(b, cons(a, _nlff_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(b, cons(a, _nlff_1)) ; h1 -> a ; l2 -> cons(_jzef_0, _jzef_1) ; t1 -> cons(_kzef_0, _kzef_1) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 17, which took 3.474502 s (model generation: 3.470600, model checking: 0.003902): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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_3(nil) <= True _r_4(a) <= True _r_5(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_5(x_1_0) append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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(a) <= True _r_5(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, cons(a, nil)) ; i -> b ; l1 -> cons(a, cons(b, _elgf_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(b, cons(a, _algf_1)) ; h1 -> a ; l2 -> cons(_jrff_0, _jrff_1) ; t1 -> cons(b, _krff_1) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 18, which took 9.824406 s (model generation: 9.817451, model checking: 0.006955): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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(a) <= True _r_5(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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(a) <= True _r_5(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, cons(b, nil)) ; i -> a ; l1 -> cons(a, _ongf_1) ; l2 -> cons(_pngf_0, _pngf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(b, nil) ; l2 -> nil ; t1 -> cons(b, nil) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 19, which took 7.751237 s (model generation: 7.748470, model checking: 0.002767): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) _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(nil, cons(x_1_0, x_1_1)) <= True _r_1(nil, nil) <= True _r_4(a) <= True _r_5(b) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, cons(a, nil)) ; i -> b ; l1 -> cons(a, cons(a, cons(b, _dfif_1))) ; l2 -> cons(_xnhf_0, _xnhf_1) } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : No: () eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 20, which took 22.565294 s (model generation: 22.560171, model checking: 0.005123): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) _r_1(nil, cons(x_1_0, x_1_1)) <= 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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_3(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_4(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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 elem(a, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(b, cons(b, nil)) ; i -> a ; l1 -> cons(a, cons(a, _ibjf_1)) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) : Yes: { _ea -> cons(a, nil) ; h1 -> a ; l2 -> cons(_slif_0, nil) ; t1 -> cons(a, nil) } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () ------------------------------------------- Step 21, which took 6.174469 s (model generation: 6.160618, model checking: 0.013851): Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(b, nil))) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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_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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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(a) <= True _r_5(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () elem(h1, cons(h1, t1)) <= True : No: () elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) : Yes: { _ja -> cons(a, nil) ; i -> b ; l1 -> cons(a, cons(b, cons(a, _tjlf_1))) ; l2 -> nil } eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) : No: () eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) : No: () False <= elem(e, nil) : No: () Total time: 60.733792 Learner time: 59.663729 Teacher time: 0.051626 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 elem(h1, cons(h1, t1)) <= True -> 0 elem(i, _ja) <= append(l1, l2, _ja) /\ elem(i, l1) -> 0 append(cons(h1, t1), l2, cons(h1, _ea)) <= append(t1, l2, _ea) -> 0 eq_elt(e, h1) \/ elem(e, cons(h1, t1)) <= elem(e, t1) -> 0 eq_elt(e, h1) \/ elem(e, t1) <= elem(e, cons(h1, t1)) -> 0 False <= elem(e, nil) -> 0 } Accumulated learning constraints: { append(cons(a, cons(a, nil)), nil, cons(a, cons(a, nil))) <= True append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= True append(cons(a, cons(b, nil)), nil, cons(a, cons(b, nil))) <= True append(cons(a, nil), cons(a, nil), cons(a, cons(a, nil))) <= True append(cons(a, nil), nil, cons(a, nil)) <= True append(cons(b, nil), cons(a, nil), cons(b, cons(a, nil))) <= True append(cons(b, nil), nil, cons(b, nil)) <= True append(nil, cons(a, nil), cons(a, nil)) <= True append(nil, cons(b, nil), cons(b, nil)) <= True append(nil, nil, nil) <= True elem(a, cons(a, nil)) <= True elem(a, cons(b, cons(a, nil))) <= True elem(a, cons(b, cons(b, cons(a, nil)))) <= True elem(b, cons(a, cons(a, cons(b, nil)))) <= True elem(b, cons(a, cons(b, nil))) <= True elem(b, cons(b, nil)) <= True False <= append(cons(a, cons(a, cons(b, nil))), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, cons(b, nil))) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(a, nil)), nil, cons(b, nil)) /\ elem(a, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, cons(a, nil))), nil, cons(a, nil)) /\ elem(b, cons(a, cons(b, cons(a, nil)))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), cons(a, nil), cons(a, nil)) False <= append(cons(a, cons(b, nil)), nil, cons(a, cons(a, nil))) False <= append(cons(a, cons(b, nil)), nil, cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(a, nil)), cons(a, nil), cons(b, cons(a, nil))) <= append(cons(a, nil), cons(a, nil), cons(a, nil)) append(cons(a, cons(a, nil)), cons(a, nil), cons(a, cons(b, cons(a, nil)))) <= append(cons(a, nil), cons(a, nil), cons(b, cons(a, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, cons(b, nil))) False <= append(cons(a, nil), cons(a, nil), cons(b, nil)) append(cons(b, cons(a, nil)), nil, cons(b, cons(a, cons(a, nil)))) <= append(cons(a, nil), nil, cons(a, cons(a, nil))) False <= append(cons(a, nil), nil, cons(b, nil)) False <= append(cons(b, cons(a, nil)), cons(a, nil), cons(b, nil)) False <= append(cons(b, cons(a, nil)), nil, cons(a, cons(a, nil))) /\ elem(b, cons(b, cons(a, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, cons(b, nil))) False <= append(cons(b, cons(a, nil)), nil, cons(b, nil)) False <= append(cons(b, nil), cons(a, nil), cons(a, cons(a, nil))) False <= append(cons(b, nil), cons(a, nil), cons(a, nil)) append(cons(b, cons(b, nil)), cons(a, nil), cons(b, cons(b, nil))) <= append(cons(b, nil), cons(a, nil), cons(b, nil)) False <= append(cons(b, nil), nil, cons(a, cons(a, nil))) False <= append(cons(b, nil), nil, cons(a, nil)) append(cons(a, nil), cons(a, nil), cons(a, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) append(cons(b, nil), cons(a, nil), cons(b, cons(b, nil))) <= append(nil, cons(a, nil), cons(b, nil)) False <= elem(a, cons(b, cons(b, nil))) False <= elem(a, cons(b, nil)) False <= elem(a, nil) False <= elem(b, cons(a, cons(a, nil))) False <= elem(b, cons(a, nil)) False <= elem(b, nil) } Current best model: |_ name: None append -> [ append : { _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_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 append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_2_1) /\ _r_5(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_3(x_2_1) /\ _r_4(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1) /\ _r_1(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_2(x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; elem -> [ elem : { _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(a) <= True _r_5(b) <= True elem(a, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) elem(a, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) elem(b, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) elem(b, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {elt, eltlist} _|