Solving ../../benchmarks/smtlib/true/isaplanner_prop27.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: { nat -> {s, z} ; natlist -> {cons, nil} } definition: { (append, F: { append(nil, l2, l2) <= True append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) } eq_natlist(_cga, _dga) <= append(_aga, _bga, _cga) /\ append(_aga, _bga, _dga) ) (member, P: { member(h, cons(h, t)) <= True eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) False <= member(e, nil) } ) } properties: { member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) } over-approximation: {append} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Solving took 60.033325 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) <= True append(nil, cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, cons(s(z), nil)), cons(z, cons(s(z), nil))) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(s(z)))), cons(s(s(s(s(z)))), nil)) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(s(z)), cons(z, cons(s(s(z)), nil))) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(s(s(z)), cons(s(s(s(z))), nil)), cons(s(s(z)), nil), cons(s(s(z)), cons(z, nil))) <= append(cons(s(s(s(z))), nil), cons(s(s(z)), nil), cons(z, nil)) append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, cons(s(z), nil)), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(s(z)), cons(z, nil)), cons(s(s(z)), nil)) /\ member(z, cons(s(s(z)), cons(z, nil))) False <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil))) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(z), nil), cons(s(s(z)), nil)) member(s(z), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, cons(z, nil)))) append(cons(s(z), nil), cons(s(z), nil), cons(s(z), cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, nil))) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, cons(s(z), nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(s(z))), cons(z, nil)) False <= member(s(s(s(z))), nil) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), cons(z, cons(s(z), nil))) False <= member(s(s(z)), cons(z, nil)) False <= member(s(s(z)), nil) member(s(z), cons(z, cons(s(s(z)), cons(z, cons(z, nil))))) <= member(s(z), cons(s(s(z)), cons(z, cons(z, nil)))) False <= member(s(z), cons(s(s(z)), nil)) member(s(z), cons(z, cons(s(z), cons(z, nil)))) <= member(s(z), cons(s(z), cons(z, nil))) member(s(z), cons(s(s(z)), cons(z, nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(z, nil)))) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(s(z)), nil))) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, 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_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_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= _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_1_1, x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ member(x_0_0, 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)) <= member(x_1_0, x_2_1) 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)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, 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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_0) /\ _r_6(x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) member(s(x_0_0), nil) <= _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; member -> [ member : { _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_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) member(s(x_0_0), nil) <= _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006699 s (model generation: 0.006359, model checking: 0.000340): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] ; member -> [ member : { } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } member(h, cons(h, t)) <= True : Yes: { h -> z } member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : No: () append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : No: () False <= member(e, nil) : No: () ------------------------------------------- Step 1, which took 0.006630 s (model generation: 0.006552, model checking: 0.000078): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True member(z, cons(z, nil)) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; member -> [ member : { member(z, cons(x_1_0, x_1_1)) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_dmlf_0, _dmlf_1) } member(h, cons(h, t)) <= True : Yes: { h -> s(_emlf_0) } member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : No: () append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> nil ; l2 -> nil ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> z ; h -> s(_jmlf_0) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 2, which took 0.008814 s (model generation: 0.008674, model checking: 0.000140): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(z), cons(s(z), nil)) <= True member(z, cons(z, nil)) <= True member(z, nil) <= member(z, cons(s(z), 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 } ] ; member -> [ member : { member(s(x_0_0), cons(x_1_0, x_1_1)) <= True member(z, cons(x_1_0, x_1_1)) <= True member(z, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : No: () append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(_lmlf_0, _lmlf_1) ; l2 -> cons(_mmlf_0, _mmlf_1) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(_rmlf_0) ; h -> z ; t -> nil } False <= member(e, nil) : Yes: { e -> z } ------------------------------------------- Step 3, which took 0.018490 s (model generation: 0.018349, model checking: 0.000141): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(z), cons(s(z), nil)) <= True member(z, cons(z, nil)) <= True member(s(z), nil) <= member(s(z), cons(z, nil)) False <= member(z, cons(s(z), nil)) False <= member(z, 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 } ] ; member -> [ member : { _r_1(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= True member(s(x_0_0), nil) <= True member(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(_onlf_0), _wmlf_1) ; e -> z ; l1 -> cons(_ymlf_0, _ymlf_1) ; l2 -> cons(z, _zmlf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> z ; h -> s(_fnlf_0) ; t -> cons(z, _gnlf_1) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : No: () False <= member(e, nil) : Yes: { e -> s(_nnlf_0) } ------------------------------------------- Step 4, which took 0.053226 s (model generation: 0.052838, model checking: 0.000388): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(z), cons(s(z), nil)) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1)) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(s(x_0_0)) <= True _r_3(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_0) member(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(z, cons(_jqlf_0, _jqlf_1)) ; e -> s(_tnlf_0) ; l1 -> cons(_unlf_0, _unlf_1) ; l2 -> cons(s(_iqlf_0), _vnlf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(_zolf_0) ; h -> z ; t -> cons(s(_iqlf_0), _bplf_1) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(_pqlf_0)) ; h -> s(z) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 5, which took 0.069951 s (model generation: 0.069443, model checking: 0.000508): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True member(s(z), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) member(s(s(z)), nil) <= member(s(s(z)), cons(s(z), nil)) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _r_2(cons(x_0_0, x_0_1)) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_1(z, s(x_1_0)) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : Yes: { h -> s(s(_iulf_0)) ; t -> nil } member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(z, nil) ; e -> s(z) ; l1 -> nil ; l2 -> cons(_rrlf_0, cons(_sulf_0, _sulf_1)) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(z) ; h -> s(s(_fvlf_0)) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 6, which took 0.153465 s (model generation: 0.152378, model checking: 0.001087): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True member(s(z), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) /\ member(s(z), cons(z, cons(z, nil))) member(s(s(z)), nil) <= member(s(s(z)), cons(s(z), nil)) False <= member(s(z), cons(s(s(z)), nil)) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _r_1(nil, z) <= 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_1_1, x_2_0) 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)) <= _r_1(x_1_1, x_2_0) append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_2(cons(x_0_0, x_0_1)) <= True _r_3(s(x_0_0)) <= _r_4(x_0_0) _r_4(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) member(s(x_0_0), nil) <= _r_3(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(_ramf_0), nil) } member(h, cons(h, t)) <= True : Yes: { h -> s(s(s(_cbmf_0))) ; t -> nil } member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(z, nil) ; e -> s(z) ; l1 -> cons(_tvlf_0, _tvlf_1) ; l2 -> cons(s(z), nil) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(z, _ixlf_1) ; h1 -> s(_uamf_0) ; l2 -> cons(_jxlf_0, nil) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> z ; h -> s(_aamf_0) ; t -> cons(s(_nbmf_0), nil) } False <= member(e, nil) : Yes: { e -> s(s(z)) } ------------------------------------------- Step 7, which took 0.309198 s (model generation: 0.307326, model checking: 0.001872): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True member(s(z), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) /\ member(s(z), cons(z, cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _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(s(x_0_0)) <= _r_4(x_0_0) _r_4(s(x_0_0)) <= _r_3(x_0_0) _r_4(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= member(x_1_0, x_2_1) 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 member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] ; member -> [ member : { _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(s(x_0_0)) <= _r_4(x_0_0) _r_4(s(x_0_0)) <= _r_3(x_0_0) _r_4(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) /\ _r_4(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(z), nil) ; e -> z ; l1 -> nil ; l2 -> cons(z, _vgmf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(z, nil) ; l2 -> cons(s(z), _ahmf_1) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(z) ; h -> z ; t -> cons(z, cons(s(z), _jpmf_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> z ; h -> s(s(z)) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 8, which took 0.968143 s (model generation: 0.967090, model checking: 0.001053): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True member(s(z), cons(z, cons(z, nil))) <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) /\ member(s(z), cons(z, cons(z, nil))) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _r_1(nil, z) <= True _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_2(s(x_0_0), nil) <= True _r_2(z, cons(x_1_0, x_1_1)) <= 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_0_0, x_2_1) 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)) <= _r_1(x_1_1, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0, x_2_1) append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_2(s(x_0_0), nil) <= True _r_2(z, cons(x_1_0, x_1_1)) <= True _r_3(s(x_0_0), s(x_1_0)) <= _r_3(x_0_0, x_1_0) _r_3(z, s(x_1_0)) <= _r_5(x_1_0) _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_5(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_0_0, x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_0) member(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(_gwmf_0), cons(s(_gwmf_0), _uwmf_1)) ; e -> z ; l1 -> cons(z, _kqmf_1) ; l2 -> cons(z, _lqmf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> z ; h -> s(_qtmf_0) ; t -> cons(s(_gwmf_0), cons(z, _cwmf_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(z) ; h -> z ; t -> cons(z, nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 9, which took 0.697336 s (model generation: 0.695538, model checking: 0.001798): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _r_4(z) <= True _r_5(s(x_0_0)) <= True 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_1_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) 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)) <= _r_4(x_1_0) /\ _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) /\ _r_5(x_2_0) append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, s(x_1_0)) <= _r_4(x_1_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(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(z) <= True _r_5(s(x_0_0)) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(_renf_0), nil) ; e -> z ; l1 -> cons(s(_senf_0), _jzmf_1) ; l2 -> cons(z, _kzmf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(_uanf_0, _uanf_1) ; h1 -> z ; l2 -> cons(s(_benf_0), _vanf_1) ; t1 -> cons(s(_senf_0), _wanf_1) } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(z)) ; h -> z ; t -> cons(s(z), cons(z, nil)) } False <= member(e, nil) : No: () ------------------------------------------- Step 10, which took 1.366169 s (model generation: 1.364393, model checking: 0.001776): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, s(x_1_0)) <= _r_5(x_1_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(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(s(x_0_0)) <= True _r_5(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= member(x_1_0, x_2_1) 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)) <= _r_4(x_1_0) /\ _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) /\ _r_5(x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; member -> [ member : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, s(x_1_0)) <= _r_5(x_1_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(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(s(x_0_0)) <= True _r_5(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(_wsnf_0), nil) ; e -> z ; l1 -> nil ; l2 -> cons(s(_vqnf_0), cons(z, _rqnf_1)) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(s(s(_lqnf_0)), nil) ; l2 -> cons(s(z), _mmnf_1) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(s(z)) ; h -> z ; t -> cons(s(s(z)), _innf_1) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(z) ; h -> z ; t -> cons(s(s(_tunf_0)), cons(z, nil)) } False <= member(e, nil) : No: () ------------------------------------------- Step 11, which took 6.576573 s (model generation: 6.567643, model checking: 0.008930): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(s(z)), cons(z, cons(s(s(z)), nil))) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(z), nil), cons(s(s(z)), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) member(s(z), cons(s(s(z)), cons(z, nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(z, nil)))) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, nil) } Current best model: |_ name: None append -> [ append : { _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_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(s(x_0_0)) <= _r_5(x_0_0) _r_5(s(x_0_0)) <= _r_4(x_0_0) _r_5(z) <= True _r_6(z) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= member(x_1_0, x_2_1) 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)) <= _r_1(x_1_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_0) /\ _r_6(x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) } ] ; member -> [ member : { _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(s(x_0_0)) <= _r_5(x_0_0) _r_5(s(x_0_0)) <= _r_4(x_0_0) _r_5(z) <= True _r_6(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_6(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(_bcpf_0), cons(_ubpf_0, _ubpf_1)) } member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(z, nil) ; e -> s(z) ; l1 -> nil ; l2 -> cons(z, cons(s(z), _zepf_1)) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(z)) ; h -> z ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 12, which took 6.151267 s (model generation: 6.149181, model checking: 0.002086): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(s(z)), cons(z, cons(s(s(z)), nil))) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(z), nil), cons(s(s(z)), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, cons(s(z), nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), cons(z, nil)) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) member(s(z), cons(s(s(z)), cons(z, nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(z, nil)))) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, 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_4(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_4(nil) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= 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) /\ _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_5(x_1_0) 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)) <= _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_1) /\ _r_5(x_1_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_1) /\ _r_6(x_1_0) /\ _r_6(x_2_0) append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_1(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, s(x_1_0)) <= _r_5(x_1_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_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_4(nil) <= True _r_5(z) <= True _r_6(s(x_0_0)) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(z, cons(s(_kwpf_0), nil)) } member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(z, cons(z, cons(z, nil))) ; e -> s(z) ; l1 -> nil ; l2 -> cons(s(z), _mppf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(_mspf_0, cons(z, _jwpf_1)) ; h1 -> s(_kwpf_0) ; l2 -> cons(s(_kwpf_0), _nspf_1) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(z) ; h -> z ; t -> cons(s(z), cons(z, nil)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(z)) ; h -> z ; t -> cons(s(z), nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 13, which took 7.210540 s (model generation: 7.182000, model checking: 0.028540): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, cons(s(z), nil)), cons(z, cons(s(z), nil))) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(s(z)), cons(z, cons(s(s(z)), nil))) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(z), nil), cons(s(s(z)), nil)) member(s(z), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, cons(z, nil)))) append(cons(s(z), nil), cons(s(z), nil), cons(s(z), cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, nil))) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, cons(s(z), nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), cons(z, cons(s(z), nil))) False <= member(s(s(z)), cons(z, nil)) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) member(s(z), cons(z, cons(s(z), cons(z, nil)))) <= member(s(z), cons(s(z), cons(z, nil))) member(s(z), cons(s(s(z)), cons(z, nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(z, nil)))) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, 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_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_6(x_0_0) _r_4(z) <= True _r_5(s(x_0_0)) <= _r_6(x_0_0) _r_6(s(x_0_0)) <= _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_2_1) /\ _r_4(x_1_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) 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)) <= _r_1(x_1_1) /\ _r_1(x_2_1) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_1) /\ _r_6(x_1_0) /\ _r_6(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_2_1) append(nil, nil, nil) <= True } ] ; member -> [ member : { _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_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_6(x_0_0) _r_4(z) <= True _r_5(s(x_0_0)) <= _r_6(x_0_0) _r_6(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_1_1) /\ _r_6(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_5(x_1_0) /\ _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(s(_aruf_0)), nil) } member(h, cons(h, t)) <= True : Yes: { h -> s(s(s(s(_dsuf_0)))) ; t -> nil } member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(_dsuf_0), nil) ; e -> z ; l1 -> cons(_ierf_0, cons(s(z), _rruf_1)) ; l2 -> cons(z, _jerf_1) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(_ldtf_0, cons(z, _eruf_1)) ; l2 -> cons(s(_aruf_0), cons(z, _eruf_1)) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : No: () eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(s(z))) ; h -> z ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 14, which took 14.032953 s (model generation: 13.834817, model checking: 0.198136): Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) <= True append(nil, cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, cons(s(z), nil)), cons(z, cons(s(z), nil))) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(s(z)))), cons(s(s(s(s(z)))), nil)) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(s(z)), cons(z, cons(s(s(z)), nil))) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, cons(s(z), nil)), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil))) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(z), nil), cons(s(s(z)), nil)) member(s(z), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, cons(z, nil)))) append(cons(s(z), nil), cons(s(z), nil), cons(s(z), cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, nil))) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, cons(s(z), nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(s(z))), nil) <= member(s(s(s(z))), cons(z, nil)) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), cons(z, cons(s(z), nil))) False <= member(s(s(z)), cons(z, nil)) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), nil)) member(s(z), cons(z, cons(s(z), cons(z, nil)))) <= member(s(z), cons(s(z), cons(z, nil))) member(s(z), cons(s(s(z)), cons(z, nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(z, nil)))) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, 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_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_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= _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_1_1, x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ member(x_0_0, 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)) <= member(x_1_0, x_2_1) 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)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, 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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_0) /\ _r_6(x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) member(s(x_0_0), nil) <= _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; member -> [ member : { _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_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) member(s(x_0_0), nil) <= _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(h, cons(h, t)) <= True : No: () member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) : Yes: { _ega -> cons(s(s(z)), nil) ; e -> z ; l1 -> nil ; l2 -> cons(s(s(z)), cons(z, _zkdg_1)) } append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) : Yes: { _zfa -> cons(z, nil) ; h1 -> s(s(z)) ; l2 -> cons(s(s(z)), nil) ; t1 -> cons(s(s(s(z))), nil) } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(z) ; h -> z ; t -> cons(s(s(z)), cons(z, cons(z, nil))) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> z ; h -> s(_dlbg_0) ; t -> cons(s(s(z)), nil) } False <= member(e, nil) : Yes: { e -> s(s(s(z))) } Total time: 60.033325 Learner time: 37.382581 Teacher time: 0.246872 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 member(h, cons(h, t)) <= True -> 0 member(e, _ega) <= append(l1, l2, _ega) /\ member(e, l2) -> 0 append(cons(h1, t1), l2, cons(h1, _zfa)) <= append(t1, l2, _zfa) -> 0 eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) -> 0 eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) -> 0 False <= member(e, nil) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(z, nil), cons(z, nil), cons(z, cons(z, nil))) <= True append(cons(z, nil), nil, cons(z, nil)) <= True append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) <= True append(nil, cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) <= True append(nil, cons(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, cons(s(z), nil)), cons(z, cons(s(z), nil))) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True member(s(s(s(s(z)))), cons(s(s(s(s(z)))), nil)) <= True member(s(s(s(z))), cons(s(s(s(z))), nil)) <= True member(s(s(z)), cons(s(s(z)), nil)) <= True member(s(s(z)), cons(z, cons(s(s(z)), nil))) <= True member(s(z), cons(s(z), nil)) <= True member(s(z), cons(z, cons(s(z), nil))) <= True member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= True member(z, cons(s(z), cons(s(z), cons(z, nil)))) <= True member(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True append(cons(s(s(z)), cons(s(s(s(z))), nil)), cons(s(s(z)), nil), cons(s(s(z)), cons(z, nil))) <= append(cons(s(s(s(z))), nil), cons(s(s(z)), nil), cons(z, nil)) append(cons(z, cons(s(z), nil)), cons(s(z), nil), cons(z, cons(z, nil))) <= append(cons(s(z), nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, cons(s(z), nil)), cons(z, nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(s(z), nil), cons(z, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(s(z)), cons(z, nil)), cons(s(s(z)), nil)) /\ member(z, cons(s(s(z)), cons(z, nil))) False <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), cons(z, nil)), cons(z, cons(z, nil))) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(z), nil), cons(s(s(z)), nil)) member(s(z), cons(z, cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, cons(z, nil)))) append(cons(s(z), nil), cons(s(z), nil), cons(s(z), cons(z, cons(z, nil)))) <= append(nil, cons(s(z), nil), cons(z, cons(z, nil))) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, cons(s(z), nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) False <= member(s(s(s(z))), cons(z, nil)) False <= member(s(s(s(z))), nil) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(z), cons(z, nil))) <= member(s(s(z)), cons(z, cons(s(z), cons(z, nil)))) False <= member(s(s(z)), cons(z, cons(s(z), nil))) False <= member(s(s(z)), cons(z, nil)) False <= member(s(s(z)), nil) member(s(z), cons(z, cons(s(s(z)), cons(z, cons(z, nil))))) <= member(s(z), cons(s(s(z)), cons(z, cons(z, nil)))) False <= member(s(z), cons(s(s(z)), nil)) member(s(z), cons(z, cons(s(z), cons(z, nil)))) <= member(s(z), cons(s(z), cons(z, nil))) member(s(z), cons(s(s(z)), cons(z, nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(z, nil)))) False <= member(s(z), cons(z, cons(z, nil))) False <= member(s(z), cons(z, nil)) False <= member(s(z), nil) False <= member(z, cons(s(s(z)), nil)) False <= member(z, cons(s(z), cons(s(s(z)), nil))) False <= member(z, cons(s(z), cons(s(z), nil))) False <= member(z, cons(s(z), nil)) False <= member(z, 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_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_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= _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_1_1, x_2_1) /\ append(x_0_1, x_1_1, x_2_1) /\ member(x_0_0, 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)) <= member(x_1_0, x_2_1) 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)) <= _r_1(x_1_1, x_2_1) /\ _r_4(x_1_0) /\ _r_4(x_2_0) append(nil, 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) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_6(x_1_0) /\ _r_6(x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) member(s(x_0_0), nil) <= _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] ; member -> [ member : { _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_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_4(s(x_0_0)) <= _r_5(x_0_0) _r_4(s(x_0_0)) <= _r_6(x_0_0) _r_5(z) <= True _r_6(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_4(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_6(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_6(x_0_0) member(s(x_0_0), nil) <= _r_6(x_0_0) member(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _|