Solving ../../benchmarks/smtlib/true/isaplanner_prop28.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, _gca)) <= append(t1, l2, _gca) } eq_natlist(_jca, _kca) <= append(_hca, _ica, _jca) /\ append(_hca, _ica, _kca) ) (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, _lca) <= append(l, cons(e, nil), _lca) } over-approximation: {append} under-approximation: {member} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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 59.290659 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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(s(z))), nil), cons(s(s(s(z))), nil)) <= True append(nil, cons(s(s(z)), nil), cons(s(s(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(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 member(s(s(z)), cons(z, nil)) <= append(cons(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)) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(z, cons(z, cons(s(z), nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, cons(s(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))) append(cons(z, nil), cons(s(s(s(z))), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(s(z))), nil), cons(s(s(z)), nil)) member(s(s(s(z))), cons(s(s(z)), nil)) <= append(nil, cons(s(s(s(z))), nil), cons(s(s(z)), nil)) False <= append(nil, cons(s(s(z)), nil), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) member(s(s(z)), cons(z, nil)) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, cons(s(s(z)), cons(s(z), nil)))) <= member(s(s(z)), cons(s(s(z)), cons(s(z), nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), cons(z, cons(s(z), nil))) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), cons(z, nil))) member(s(z), cons(s(s(z)), cons(s(z), nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(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_5(x_1_0) _r_1(z, z) <= 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(z) <= True _r_5(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)) <= 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_0, 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) /\ _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_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_4(x_1_0) } ] ; member -> [ member : { _r_1(s(x_0_0), s(x_1_0)) <= _r_5(x_1_0) _r_1(z, z) <= 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(z) <= True _r_5(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_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_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.006559 s (model generation: 0.006495, model checking: 0.000064): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(e, _lca) <= append(l, cons(e, nil), _lca) : No: () append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : 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.006572 s (model generation: 0.006500, model checking: 0.000072): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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 } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] ; member -> [ member : { } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_rkdh_0, _rkdh_1) } member(e, _lca) <= append(l, cons(e, nil), _lca) : No: () append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> 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)) : No: () False <= member(e, nil) : No: () ------------------------------------------- Step 2, which took 0.008176 s (model generation: 0.008104, model checking: 0.000072): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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 } 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 : { } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(_ykdh_0, _ykdh_1) ; e -> z ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(_bldh_0, _bldh_1) ; l2 -> cons(_cldh_0, _cldh_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)) : No: () False <= member(e, nil) : No: () ------------------------------------------- Step 3, which took 0.011935 s (model generation: 0.011857, model checking: 0.000078): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(z, cons(z, nil)) <= True } 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 : { 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 : No: () member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(_hldh_0, _hldh_1) ; e -> s(_ildh_0) ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : 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 -> z ; h -> s(_lldh_0) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 4, which took 0.014385 s (model generation: 0.014309, model checking: 0.000076): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(z, cons(z, nil)) <= True member(s(z), cons(z, nil)) <= append(nil, cons(s(z), nil), cons(z, nil)) member(z, nil) <= member(z, cons(s(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 : { 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(e, _lca) <= append(l, cons(e, nil), _lca) : No: () append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : 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(_qldh_0) ; h -> z ; t -> nil } False <= member(e, nil) : Yes: { e -> z } ------------------------------------------- Step 5, which took 0.018844 s (model generation: 0.018732, model checking: 0.000112): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(z, cons(z, nil)) <= True member(s(z), cons(z, nil)) <= append(nil, cons(s(z), nil), cons(z, nil)) 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(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(_kmdh_0), _xldh_1) ; e -> z ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> z ; h -> s(_bmdh_0) ; t -> cons(z, _cmdh_1) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : No: () False <= member(e, nil) : Yes: { e -> s(_jmdh_0) } ------------------------------------------- Step 6, which took 0.031445 s (model generation: 0.031101, model checking: 0.000344): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(z, cons(s(z), cons(z, nil))) <= True member(z, cons(z, nil)) <= True False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(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_2(z) <= 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)) <= True append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_2(x_2_0) append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_1(cons(x_0_0, x_0_1)) <= True _r_2(z) <= True member(z, cons(x_1_0, x_1_1)) <= _r_1(x_1_1) member(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(_sndh_0), _nmdh_1) } member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(_omdh_0, _omdh_1) ; e -> s(_pmdh_0) ; l -> cons(_qmdh_0, _qmdh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : 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 -> z ; h -> s(_hndh_0) ; t -> cons(s(_vndh_0), nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 7, which took 0.059340 s (model generation: 0.058963, model checking: 0.000377): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(s(z), nil), cons(s(z), nil)) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, 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, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(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), 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)) <= True _r_1(z, 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_0, 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_0, x_2_0) append(nil, nil, nil) <= True } ] ; member -> [ member : { _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(z) <= True 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(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(_ipdh_0), _yndh_1) ; e -> s(_zndh_0) ; l -> cons(_aodh_0, _aodh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(z, _nodh_1) ; h1 -> s(_opdh_0) ; l2 -> cons(z, _oodh_1) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> z ; h -> s(_rodh_0) ; t -> cons(s(_tpdh_0), cons(z, _spdh_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : No: () False <= member(e, nil) : No: () ------------------------------------------- Step 8, which took 0.108494 s (model generation: 0.108143, model checking: 0.000351): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(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 member(s(z), cons(s(z), nil)) <= append(cons(z, nil), cons(s(z), nil), cons(s(z), nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(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(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(s(x_0_0), s(x_1_0)) <= True _r_1(z, z) <= True _r_3(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_3(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_1(x_1_0, x_2_0) append(nil, nil, nil) <= True } ] ; 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_3(x_0_0) _r_3(z) <= True 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(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(_krdh_0), _gqdh_1) ; e -> s(_hqdh_0) ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(s(_mrdh_0), _pqdh_1) ; l2 -> cons(s(_lrdh_0), _qqdh_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)) : No: () False <= member(e, nil) : No: () ------------------------------------------- Step 9, which took 0.153461 s (model generation: 0.152743, model checking: 0.000718): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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(s(z), nil), cons(z, cons(s(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(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, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(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), 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_2(x_0_0) _r_2(z) <= True _r_3(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)) <= 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_2(x_1_0) /\ _r_2(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_3(x_1_0) /\ _r_3(x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(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_2(x_1_0) } ] ; 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_2(x_0_0) _r_2(z) <= True _r_3(s(x_0_0)) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(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_2(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(z, cons(s(_avdh_0), _kvdh_1)) ; e -> s(_gsdh_0) ; l -> cons(_hsdh_0, _hsdh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(z, cons(s(_avdh_0), _tudh_1)) ; l2 -> cons(s(_sudh_0), _ysdh_1) ; t1 -> cons(_zsdh_0, _zsdh_1) } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(_jtdh_0) ; h -> z ; t -> cons(s(_zudh_0), _ltdh_1) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(_hvdh_0)) ; h -> s(z) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 10, which took 0.748796 s (model generation: 0.747848, model checking: 0.000948): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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(z), cons(s(z), nil)) <= True member(s(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, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(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), 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)) <= True _r_3(z) <= True _r_4(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) 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_1_0) /\ _r_3(x_2_0) 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, 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_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= True _r_3(z) <= True _r_4(s(x_0_0)) <= 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_4(x_1_0) member(s(x_0_0), nil) <= _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_3(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(_fzdh_0), cons(s(_fzdh_0), nil)) ; e -> z ; l -> cons(_uvdh_0, _uvdh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : No: () eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(s(_czdh_0)) ; h -> z ; t -> nil } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(_qzdh_0)) ; h -> s(z) ; t -> cons(z, nil) } False <= member(e, nil) : Yes: { e -> s(s(_czdh_0)) } ------------------------------------------- Step 11, which took 0.697070 s (model generation: 0.695468, model checking: 0.001602): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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(z), cons(s(z), nil)) <= True member(s(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, nil)) False <= append(cons(z, nil), cons(z, nil), cons(s(z), cons(s(z), nil))) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(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_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)) <= True _r_3(z) <= True _r_4(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)) <= 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_3(x_1_0) /\ _r_3(x_2_0) 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, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(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) } ] ; 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_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= True _r_3(z) <= True _r_4(s(x_0_0)) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_1_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(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(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(_zheh_0), cons(z, cons(_vheh_0, _vheh_1))) ; e -> s(s(_oieh_0)) ; l -> cons(_iaeh_0, _iaeh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(s(_aieh_0), cons(z, cons(_vheh_0, _vheh_1))) ; l2 -> cons(s(s(_aieh_0)), _ubeh_1) ; t1 -> cons(_vbeh_0, _vbeh_1) } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(s(z)) ; h -> s(s(s(_xieh_0))) ; t -> cons(z, cons(_uheh_0, _uheh_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(_zheh_0)) ; h -> z ; t -> cons(_jeeh_0, nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 12, which took 2.127015 s (model generation: 2.125509, model checking: 0.001506): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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(z), cons(s(z), nil)) <= True member(s(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(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), 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(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(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_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)) <= True _r_3(z) <= True _r_4(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)) <= 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_3(x_1_0) /\ _r_3(x_2_0) 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, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(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) } ] ; 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_3(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= True _r_3(z) <= True _r_4(s(x_0_0)) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_2(x_1_1) /\ _r_3(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(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(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(_hreh_0), _qkeh_1) ; e -> s(s(_cseh_0)) ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(s(_qreh_0), _fleh_1) ; l2 -> cons(s(s(_freh_0)), _gleh_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(z) ; h -> z ; t -> cons(z, nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 13, which took 1.676736 s (model generation: 1.675115, model checking: 0.001621): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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(z), cons(s(z), nil)) <= True member(s(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(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), 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(nil, cons(s(s(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)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(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(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_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(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_3(x_1_0) /\ _r_3(x_2_0) 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, 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_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_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(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_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 : Yes: { l2 -> cons(s(s(_sxeh_0)), _sseh_1) } member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(z, cons(z, cons(s(z), _yzeh_1))) ; e -> s(_useh_0) ; l -> cons(_vseh_0, _vseh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(_uteh_0, cons(z, cons(s(z), _uzeh_1))) ; l2 -> cons(s(s(_sxeh_0)), _vteh_1) ; t1 -> cons(_wteh_0, _wteh_1) } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(s(_ayeh_0)) ; h -> z ; t -> cons(z, cons(s(z), _hyeh_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(s(_ayeh_0)) ; h -> z ; t -> cons(s(z), nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 14, which took 4.187179 s (model generation: 4.185215, model checking: 0.001964): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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), nil), cons(s(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(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(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(z, cons(z, cons(s(z), nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, cons(s(z), nil)))) member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, cons(s(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(nil, cons(s(s(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)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), cons(z, cons(s(z), nil))) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(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(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_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(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)) <= _r_3(x_1_0) /\ _r_3(x_2_0) 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, 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_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_1(x_0_1) _r_1(cons(x_0_0, x_0_1)) <= _r_4(x_0_0) _r_2(cons(x_0_0, x_0_1)) <= _r_2(x_0_1) _r_2(cons(x_0_0, x_0_1)) <= _r_3(x_0_0) _r_3(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) /\ _r_4(x_0_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(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(z, nil) ; e -> s(s(z)) ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(z, nil) ; l2 -> cons(s(s(z)), _dcfh_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 -> z ; h -> s(s(z)) ; t -> nil } False <= member(e, nil) : No: () ------------------------------------------- Step 15, which took 8.252566 s (model generation: 8.250492, model checking: 0.002074): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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), nil), cons(s(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(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(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(z, cons(z, cons(s(z), nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, cons(s(z), nil)))) member(s(z), cons(z, cons(z, cons(s(z), nil)))) <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, cons(s(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(nil, cons(s(s(z)), nil), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) member(s(s(z)), cons(z, nil)) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), cons(z, cons(s(z), nil))) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(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, z) <= 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_5(x_0_0) _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_1(x_1_0, 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_0_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_2_1) /\ _r_5(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_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_1(x_1_0, x_2_0) append(nil, nil, nil) <= True } ] ; 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_5(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_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_5(x_1_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 : No: () member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(_ymfh_0, nil) ; e -> s(s(_rvfh_0)) ; l -> cons(s(_svfh_0), _anfh_1) } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(z, _lofh_1) ; h1 -> z ; l2 -> cons(s(_jwfh_0), _mofh_1) ; t1 -> cons(s(_gwfh_0), nil) } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(z) ; h -> z ; t -> cons(z, cons(s(_qvfh_0), _ewfh_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(z) ; h -> s(s(_fxfh_0)) ; t -> cons(z, nil) } False <= member(e, nil) : No: () ------------------------------------------- Step 16, which took 13.529825 s (model generation: 13.527267, model checking: 0.002558): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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), nil), cons(s(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(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 member(s(s(z)), cons(z, nil)) <= append(cons(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)) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(z, cons(z, cons(s(z), nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, cons(s(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(nil, cons(s(s(z)), nil), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) member(s(s(z)), cons(z, nil)) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), cons(z, cons(s(z), nil))) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(s(s(z)), nil) False <= member(s(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(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0, x_1_0) _r_1(z, z) <= 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(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_0, x_2_0) append(nil, nil, nil) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_5(x_0_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_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_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(z) <= True member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_1) /\ _r_5(x_0_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_5(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(s(z)), nil) ; e -> s(s(z)) ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(s(s(z)), _oyfh_1) ; l2 -> cons(s(s(z)), _pyfh_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)) : No: () False <= member(e, nil) : No: () ------------------------------------------- Step 17, which took 16.613991 s (model generation: 16.608907, model checking: 0.005084): Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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), nil), cons(s(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(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 member(s(s(z)), cons(z, nil)) <= append(cons(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)) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(z, cons(z, cons(s(z), nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, cons(s(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(nil, cons(s(s(z)), nil), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) member(s(s(z)), cons(z, nil)) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), cons(z, cons(s(z), nil))) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(s(s(z)), nil) False <= member(s(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(s(x_0_0), s(x_1_0)) <= _r_5(x_1_0) _r_1(z, z) <= 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(z) <= True _r_5(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)) <= 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_0, 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) /\ _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_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_4(x_1_0) } ] ; member -> [ member : { _r_1(s(x_0_0), s(x_1_0)) <= _r_5(x_1_0) _r_1(z, z) <= 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(z) <= True _r_5(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_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_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(s(s(_pbhh_0))), _righ_1) } member(e, _lca) <= append(l, cons(e, nil), _lca) : Yes: { _lca -> cons(s(s(z)), nil) ; e -> s(s(s(_ubhh_0))) ; l -> nil } append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) : Yes: { _gca -> cons(s(s(z)), nil) ; l2 -> cons(s(s(s(_pbhh_0))), _zlgh_1) ; t1 -> nil } eq_nat(e, h) \/ member(e, cons(h, t)) <= member(e, t) : Yes: { e -> s(s(_ldhh_0)) ; h -> z ; t -> cons(s(s(z)), cons(s(z), _mzgh_1)) } eq_nat(e, h) \/ member(e, t) <= member(e, cons(h, t)) : Yes: { e -> s(z) ; h -> z ; t -> cons(s(s(_ubhh_0)), cons(s(z), _mzgh_1)) } False <= member(e, nil) : No: () Total time: 59.290659 Learner time: 48.232769 Teacher time: 0.019620 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 member(e, _lca) <= append(l, cons(e, nil), _lca) -> 0 append(cons(h1, t1), l2, cons(h1, _gca)) <= append(t1, l2, _gca) -> 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, cons(z, nil)), cons(s(z), nil), cons(z, cons(z, cons(s(z), nil)))) <= True append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= True append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(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(s(z))), nil), cons(s(s(s(z))), nil)) <= True append(nil, cons(s(s(z)), nil), cons(s(s(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(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 member(s(s(z)), cons(z, nil)) <= append(cons(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)) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(s(z), cons(z, cons(z, nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) member(s(s(z)), cons(s(z), cons(z, cons(z, nil)))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(s(z), cons(z, cons(z, nil)))) append(cons(z, cons(z, nil)), cons(s(s(z)), nil), cons(z, cons(z, cons(z, cons(s(z), nil))))) <= append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, cons(s(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))) append(cons(z, nil), cons(s(s(s(z))), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(s(z))), nil), cons(s(s(z)), nil)) member(s(s(s(z))), cons(s(s(z)), nil)) <= append(nil, cons(s(s(s(z))), nil), cons(s(s(z)), nil)) False <= append(nil, cons(s(s(z)), nil), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(z, nil))) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) member(s(s(z)), cons(z, nil)) <= append(nil, cons(s(s(z)), nil), cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) member(s(s(z)), cons(z, cons(s(s(z)), cons(s(z), nil)))) <= member(s(s(z)), cons(s(s(z)), cons(s(z), nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(s(z), cons(z, nil))) False <= member(s(s(z)), cons(s(z), nil)) False <= member(s(s(z)), cons(z, cons(s(z), nil))) member(s(s(z)), cons(s(s(s(z))), cons(z, cons(z, nil)))) <= member(s(s(z)), cons(z, cons(z, nil))) member(s(s(z)), cons(z, nil)) <= member(s(s(z)), cons(z, cons(z, nil))) False <= member(s(s(z)), nil) False <= member(s(z), cons(s(s(z)), cons(z, nil))) member(s(z), cons(s(s(z)), cons(s(z), nil))) <= member(s(z), cons(z, cons(s(s(z)), cons(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_5(x_1_0) _r_1(z, z) <= 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(z) <= True _r_5(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)) <= 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_0, 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) /\ _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_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_4(x_1_0) } ] ; member -> [ member : { _r_1(s(x_0_0), s(x_1_0)) <= _r_5(x_1_0) _r_1(z, z) <= 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(z) <= True _r_5(s(x_0_0)) <= _r_4(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_2(x_1_1) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_1(x_0_0, x_1_0) /\ _r_5(x_0_0) member(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_5(x_1_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_4(x_1_0) } ] -- Equality automata are defined for: {nat, natlist} _|