Solving ../../benchmarks/smtlib/true/append_equal_nat.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, _do)) <= append(t1, l2, _do) } eq_natlist(_go, _ho) <= append(_eo, _fo, _go) /\ append(_eo, _fo, _ho) ) } properties: { eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) } over-approximation: {append} under-approximation: {} Clause system for inference is: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Solving took 60.984717 seconds. Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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, cons(z, nil)), cons(z, nil), cons(z, cons(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), 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(z, nil)), cons(z, cons(z, nil))) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(s(z)), nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(nil, cons(z, nil), cons(s(z), cons(z, nil))) False <= append(cons(s(s(z)), nil), cons(z, nil), cons(s(s(z)), cons(z, nil))) /\ append(cons(z, nil), cons(s(s(z)), cons(z, nil)), cons(z, cons(s(z), nil))) /\ append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(s(z)), nil), nil, cons(z, nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, nil)), cons(s(z), nil), cons(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, cons(z, nil))) append(cons(s(z), cons(z, nil)), cons(z, cons(z, nil)), cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(z, nil))) /\ append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) append(cons(s(z), nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, s(x_1_0)) <= _r_4(x_1_0) _r_1(nil, z) <= True _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_2(s(x_0_0), nil) <= _r_3(x_0_0) _r_2(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _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_1(x_0_1, x_1_0) /\ _r_1(x_1_1, x_2_0) /\ _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_1(x_1_1, x_2_0) /\ _r_2(x_1_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)) <= _r_2(x_1_0, 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_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_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 } ] -- Equality automata are defined for: {nat, natlist} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005946 s (model generation: 0.005909, model checking: 0.000037): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None append -> [ append : { } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> nil } eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : No: () append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : No: () ------------------------------------------- Step 1, which took 0.006036 s (model generation: 0.005997, model checking: 0.000039): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(nil, nil, nil) <= True } Current best model: |_ name: None append -> [ append : { append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(_szc_0, _szc_1) } eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : No: () append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> nil ; l2 -> nil ; t1 -> nil } ------------------------------------------- Step 2, which took 0.007118 s (model generation: 0.007059, model checking: 0.000059): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 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 } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(_kad_0, _kad_1) ; _ko -> cons(_lad_0, _lad_1) ; _lo -> cons(_mad_0, _mad_1) ; i -> z ; j -> s(_oad_0) ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(_rad_0, _rad_1) ; l2 -> cons(_sad_0, _sad_1) ; t1 -> nil } ------------------------------------------- Step 3, which took 0.019043 s (model generation: 0.018868, model checking: 0.000175): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 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 False <= append(cons(s(z), nil), nil, cons(z, nil)) } Current best model: |_ name: None append -> [ append : { _r_1(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)) <= _r_1(x_0_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(_ycd_0, _ycd_1) ; _ko -> cons(_zcd_0, _zcd_1) ; _lo -> cons(_add_0, _add_1) ; i -> z ; j -> s(_cdd_0) ; l1 -> nil ; l2 -> cons(_edd_0, _edd_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> nil ; h1 -> s(_ged_0) ; l2 -> nil ; t1 -> nil } ------------------------------------------- Step 4, which took 0.020576 s (model generation: 0.020328, model checking: 0.000248): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, 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(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(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_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= True append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(_did_0), _zgd_1) ; _ko -> cons(z, _ahd_1) ; _lo -> cons(_bhd_0, _bhd_1) ; i -> s(_chd_0) ; j -> z ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : No: () ------------------------------------------- Step 5, which took 0.020859 s (model generation: 0.020580, model checking: 0.000279): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, 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(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(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_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) 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 } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, _uid_1) ; _ko -> cons(s(_cmd_0), _vid_1) ; _lo -> cons(z, _wid_1) ; i -> z ; j -> s(_yid_0) ; l1 -> cons(z, _zid_1) ; l2 -> cons(_ajd_0, _ajd_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : No: () ------------------------------------------- Step 6, which took 0.023756 s (model generation: 0.023354, model checking: 0.000402): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), nil, 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(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(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_0_0, x_2_0) /\ _r_1(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) 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 } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(_tqd_0), _qod_1) ; _ko -> cons(s(_rqd_0), _rod_1) ; _lo -> cons(s(_sqd_0), _sod_1) ; i -> s(z) ; j -> s(s(_uqd_0)) ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(z, _xpd_1) ; h1 -> s(_brd_0) ; l2 -> cons(z, _ypd_1) ; t1 -> nil } ------------------------------------------- Step 7, which took 0.026529 s (model generation: 0.026041, model checking: 0.000488): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, 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(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ append(nil, cons(s(z), nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(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)) <= 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_0_0, x_2_0) /\ _r_1(x_1_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) 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 } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, _cud_1) ; _ko -> cons(s(z), _dud_1) ; _lo -> cons(s(z), _eud_1) ; i -> z ; j -> s(z) ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(s(z), _sud_1) ; h1 -> z ; l2 -> cons(s(z), _tud_1) ; t1 -> nil } ------------------------------------------- Step 8, which took 0.080557 s (model generation: 0.080088, model checking: 0.000469): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, 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(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) /\ append(nil, cons(s(z), nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, nil), cons(s(z), nil), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), nil), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(s(z), nil)) /\ append(nil, cons(z, nil), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(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_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)) <= _r_1(x_0_0, x_2_0) /\ _r_2(x_1_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(_fae_0), _gwd_1) } eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : No: () append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : No: () ------------------------------------------- Step 9, which took 0.095994 s (model generation: 0.095646, model checking: 0.000348): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, 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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(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)) <= True append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_0) 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 } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, _wbe_1) ; _ko -> cons(s(z), _xbe_1) ; _lo -> cons(_ybe_0, cons(_mee_0, _mee_1)) ; i -> z ; j -> s(z) ; l1 -> cons(_bce_0, _bce_1) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : No: () ------------------------------------------- Step 10, which took 0.205204 s (model generation: 0.204815, model checking: 0.000389): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, 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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, 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, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_0) _r_1(z, cons(x_1_0, x_1_1)) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(z, z) <= True _r_3(z, s(x_1_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_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, 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_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, cons(_kie_0, _kie_1)) ; _ko -> cons(z, cons(_kie_0, _kie_1)) ; _lo -> cons(_xee_0, cons(_kie_0, _kie_1)) ; i -> s(_yee_0) ; j -> z ; l1 -> cons(_afe_0, _afe_1) ; l2 -> cons(z, _bfe_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(s(s(z)), _xhe_1) ; l2 -> cons(s(s(z)), _yhe_1) ; t1 -> nil } ------------------------------------------- Step 11, which took 0.489225 s (model generation: 0.488724, model checking: 0.000501): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, 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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(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)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_1(z, cons(x_1_0, x_1_1)) <= True _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(z, 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)) <= _r_1(x_1_0, x_2_1) /\ _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, 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_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(z), _yje_1) ; _ko -> cons(z, _zje_1) ; _lo -> cons(z, cons(s(_dne_0), _pne_1)) ; i -> s(z) ; j -> z ; l1 -> cons(z, _dke_1) ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(z, cons(s(_dne_0), _mne_1)) ; l2 -> cons(s(_kne_0), _dme_1) ; t1 -> cons(z, _eme_1) } ------------------------------------------- Step 12, which took 0.729801 s (model generation: 0.719068, model checking: 0.010733): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(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)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), nil) <= _r_2(x_0_0) _r_1(z, cons(x_1_0, x_1_1)) <= _r_2(x_1_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)) <= _r_1(x_0_0, x_2_1) /\ _r_2(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_1_0) /\ append(x_0_1, x_1_1, 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_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0) 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, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, nil) ; _ko -> cons(z, cons(z, _uxj_1)) ; _lo -> cons(z, _rei_1) ; i -> s(z) ; j -> z ; l1 -> nil ; l2 -> cons(z, _vei_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> nil ; h1 -> s(s(_txj_0)) ; l2 -> nil ; t1 -> nil } ------------------------------------------- Step 13, which took 0.743593 s (model generation: 0.731109, model checking: 0.012484): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(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)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), nil) <= _r_3(x_0_0) _r_1(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_2(s(x_0_0)) <= True _r_3(s(x_0_0)) <= _r_2(x_0_0) _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_1(x_0_0, x_2_1) /\ _r_3(x_0_0) /\ _r_3(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_2(x_1_0) /\ append(x_0_1, x_1_1, 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_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(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, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(_lnp_0), _wyn_1) ; _ko -> cons(s(_lnp_0), _xyn_1) ; _lo -> cons(s(_lnp_0), _yyn_1) ; i -> z ; j -> s(_azn_0) ; l1 -> nil ; l2 -> cons(_czn_0, _czn_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(z, nil) ; h1 -> z ; l2 -> cons(s(z), nil) ; t1 -> cons(s(z), nil) } ------------------------------------------- Step 14, which took 1.191329 s (model generation: 1.173613, model checking: 0.017716): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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 False <= append(cons(s(s(z)), nil), nil, cons(s(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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(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)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_1(s(x_0_0), nil) <= _r_3(x_0_0) _r_1(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_2(s(x_0_0)) <= True _r_3(s(x_0_0)) <= _r_2(x_0_0) _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_1(x_0_0, x_2_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_0_0) /\ _r_3(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_2(x_1_0) /\ _r_3(x_0_0) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(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, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(_uov_0), cons(z, _vov_1)) ; _ko -> cons(s(_uov_0), cons(_sov_0, _sov_1)) ; _lo -> cons(s(_uov_0), cons(_nov_0, _nov_1)) ; i -> z ; j -> s(_axp_0) ; l1 -> cons(s(_mov_0), _bxp_1) ; l2 -> cons(_cxp_0, _cxp_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(s(z), _mlv_1) ; h1 -> z ; l2 -> cons(s(z), cons(z, _eqv_1)) ; t1 -> nil } ------------------------------------------- Step 15, which took 1.788133 s (model generation: 1.755202, model checking: 0.032931): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), 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)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), nil) <= _r_3(x_0_0) _r_1(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_2(s(x_0_0)) <= True _r_3(s(x_0_0)) <= _r_2(x_0_0) _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_1(x_0_0, x_1_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_0_0) /\ _r_3(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_2(x_1_0) /\ _r_3(x_0_0) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(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, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(_hcja_0), cons(z, _gcja_1)) ; _ko -> cons(s(_hcja_0), nil) ; _lo -> cons(s(_hcja_0), _jfga_1) ; i -> z ; j -> s(z) ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(z, _ylia_1) ; h1 -> s(z) ; l2 -> cons(z, cons(_bija_0, _bija_1)) ; t1 -> nil } ------------------------------------------- Step 16, which took 2.081912 s (model generation: 2.042924, model checking: 0.038988): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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 False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(z, nil))) /\ append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) append(cons(s(z), nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), nil) <= _r_3(x_0_0) _r_1(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_2(s(x_0_0)) <= True _r_3(s(x_0_0)) <= _r_2(x_0_0) _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_1(x_0_0, x_1_1) /\ _r_3(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_0, x_2_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_3(x_0_0) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_0_0) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_0, x_2_1) /\ _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, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(s(z), cons(_bkwa_0, _bkwa_1)) } eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, _yita_1) ; _ko -> cons(z, cons(z, _hkwa_1)) ; _lo -> cons(s(_skwa_0), cons(z, _hkwa_1)) ; i -> z ; j -> s(s(_skwa_0)) ; l1 -> nil ; l2 -> cons(z, cons(z, _qkwa_1)) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(s(z), cons(z, _fmwa_1)) ; h1 -> s(z) ; l2 -> cons(z, cons(_bkwa_0, _bkwa_1)) ; t1 -> cons(z, _exva_1) } ------------------------------------------- Step 17, which took 3.204105 s (model generation: 3.134884, model checking: 0.069221): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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), 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 False <= append(cons(s(s(z)), nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(nil, cons(z, nil), cons(s(z), cons(z, nil))) False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) False <= append(cons(z, nil), cons(s(z), nil), cons(z, cons(z, nil))) append(cons(s(z), cons(z, nil)), cons(z, cons(z, nil)), cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(z, nil))) /\ append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) append(cons(s(z), nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(s(x_0_0), cons(x_1_0, x_1_1)) <= True _r_1(s(x_0_0), nil) <= _r_3(x_0_0) _r_1(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _r_2(s(x_0_0)) <= True _r_3(s(x_0_0)) <= _r_2(x_0_0) _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_1(x_0_0, x_1_1) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_1_1) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_3(x_0_0) /\ _r_3(x_1_0) /\ _r_3(x_2_0) append(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_2(x_1_0) /\ _r_3(x_0_0) /\ append(x_0_1, x_1_1, x_2_1) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_0, x_2_1) /\ _r_2(x_0_0) /\ _r_2(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_3(x_0_0) /\ _r_3(x_2_0) append(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, cons(x_2_0, x_2_1)) <= _r_2(x_2_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(z, _ywib_1) ; _ko -> cons(z, _zwib_1) ; _lo -> cons(z, _axib_1) ; i -> s(s(_xdkb_0)) ; j -> z ; l1 -> nil ; l2 -> nil } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(s(z), nil) ; h1 -> z ; l2 -> cons(s(z), nil) ; t1 -> cons(z, nil) } ------------------------------------------- Step 18, which took 24.995449 s (model generation: 24.994298, model checking: 0.001151): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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), 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 False <= append(cons(s(s(z)), nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(nil, cons(z, nil), cons(s(z), cons(z, nil))) False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(s(z)), nil), nil, cons(z, nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, nil)), cons(s(z), nil), cons(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, cons(z, nil))) append(cons(s(z), cons(z, nil)), cons(z, cons(z, nil)), cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(z, nil))) /\ append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) append(cons(s(z), nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), s(x_1_0), cons(x_2_0, x_2_1)) <= True _r_1(nil, s(x_1_0), cons(x_2_0, x_2_1)) <= _r_4(x_2_0) _r_1(nil, z, cons(x_2_0, x_2_1)) <= _r_3(x_2_0) _r_2(s(x_0_0), s(x_1_0)) <= _r_2(x_0_0, x_1_0) _r_2(z, z) <= 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_1(x_0_1, x_1_0, x_2_1) /\ _r_2(x_0_0, x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, 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_0) append(nil, nil, nil) <= True } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : No: () eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) : Yes: { _io -> cons(s(z), cons(z, _lcub_1)) ; _ko -> cons(s(s(z)), cons(z, _lcub_1)) ; _lo -> cons(z, cons(s(_adub_0), _sfub_1)) ; i -> s(z) ; j -> s(s(z)) ; l1 -> cons(z, nil) ; l2 -> cons(z, _pytb_1) } append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) : Yes: { _do -> cons(z, cons(z, _qdub_1)) ; l2 -> cons(z, _qbub_1) ; t1 -> cons(z, nil) } ------------------------------------------- Step 19, which took 24.233498 s (model generation: 24.194573, model checking: 0.038925): Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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, cons(z, nil)), cons(z, nil), cons(z, cons(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), 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 False <= append(cons(s(s(z)), nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(nil, cons(z, nil), cons(s(z), cons(z, nil))) False <= append(cons(s(s(z)), nil), cons(z, nil), cons(s(s(z)), cons(z, nil))) /\ append(cons(z, nil), cons(s(s(z)), cons(z, nil)), cons(z, cons(s(z), nil))) /\ append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(s(z)), nil), nil, cons(z, nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, nil)), cons(s(z), nil), cons(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, cons(z, nil))) append(cons(s(z), cons(z, nil)), cons(z, cons(z, nil)), cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(z, nil))) /\ append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) append(cons(s(z), nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, s(x_1_0)) <= _r_4(x_1_0) _r_1(nil, z) <= True _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_2(s(x_0_0), nil) <= _r_3(x_0_0) _r_2(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _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_1(x_0_1, x_1_0) /\ _r_1(x_1_1, x_2_0) /\ _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_1(x_1_1, x_2_0) /\ _r_2(x_1_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)) <= _r_2(x_1_0, 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_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_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 } ] -- Equality automata are defined for: {nat, natlist} _| Answer of teacher: append(nil, l2, l2) <= True : Yes: { l2 -> cons(z, cons(_oekc_0, _oekc_1)) } Total time: 60.984717 Learner time: 59.743080 Teacher time: 0.225583 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { append(nil, l2, l2) <= True -> 0 eq_nat(i, j) <= append(l1, _io, _lo) /\ append(l1, _ko, _lo) /\ append(cons(i, nil), l2, _io) /\ append(cons(j, nil), l2, _ko) -> 0 append(cons(h1, t1), l2, cons(h1, _do)) <= append(t1, l2, _do) -> 0 } Accumulated learning constraints: { append(cons(s(s(z)), nil), nil, cons(s(s(z)), nil)) <= True append(cons(s(z), nil), cons(z, nil), cons(s(z), cons(z, nil))) <= True append(cons(s(z), nil), nil, cons(s(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, cons(z, nil)), cons(z, nil), cons(z, cons(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), 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(z, nil)), cons(z, cons(z, nil))) <= True append(nil, cons(z, nil), cons(z, nil)) <= True append(nil, nil, nil) <= True False <= append(cons(s(s(z)), nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(nil, cons(z, nil), cons(s(z), cons(z, nil))) False <= append(cons(s(s(z)), nil), cons(z, nil), cons(s(s(z)), cons(z, nil))) /\ append(cons(z, nil), cons(s(s(z)), cons(z, nil)), cons(z, cons(s(z), nil))) /\ append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) False <= append(cons(s(s(z)), nil), nil, cons(s(z), nil)) False <= append(cons(s(s(z)), nil), nil, cons(z, nil)) False <= append(cons(s(z), nil), cons(s(z), cons(z, nil)), cons(s(z), cons(z, nil))) /\ append(cons(z, nil), cons(z, nil), cons(s(z), 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)) /\ append(cons(z, nil), cons(s(z), nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(s(z), nil)) /\ append(cons(z, nil), cons(z, nil), cons(s(z), nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, cons(z, nil))) /\ append(cons(z, nil), cons(z, cons(z, nil)), cons(z, cons(z, nil))) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(cons(z, nil), cons(z, nil), cons(z, nil)) False <= append(cons(s(z), nil), cons(z, nil), cons(z, nil)) /\ append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(cons(s(z), nil), nil, cons(z, nil)) append(cons(z, cons(z, nil)), cons(s(z), nil), cons(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, cons(z, nil))) append(cons(s(z), cons(z, nil)), cons(z, cons(z, nil)), cons(s(z), cons(s(z), cons(z, nil)))) <= append(cons(z, nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) False <= append(cons(z, nil), cons(z, nil), cons(z, cons(s(z), nil))) False <= append(cons(z, nil), nil, cons(s(z), cons(z, nil))) /\ append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) append(cons(z, nil), cons(s(s(z)), nil), cons(z, cons(s(s(z)), nil))) <= append(nil, cons(s(s(z)), nil), cons(s(s(z)), nil)) append(cons(z, nil), cons(s(z), cons(z, nil)), cons(z, cons(s(z), nil))) <= append(nil, cons(s(z), cons(z, nil)), cons(s(z), nil)) False <= append(nil, cons(s(z), nil), cons(z, nil)) append(cons(s(z), nil), cons(z, cons(z, nil)), cons(s(z), cons(z, nil))) <= append(nil, cons(z, cons(z, nil)), cons(z, nil)) False <= append(nil, cons(z, nil), cons(s(z), nil)) } Current best model: |_ name: None append -> [ append : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, s(x_1_0)) <= _r_4(x_1_0) _r_1(nil, z) <= True _r_2(s(x_0_0), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_4(x_1_0) _r_2(s(x_0_0), nil) <= _r_3(x_0_0) _r_2(z, cons(x_1_0, x_1_1)) <= _r_3(x_1_0) _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_1(x_0_1, x_1_0) /\ _r_1(x_1_1, x_2_0) /\ _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_1(x_1_1, x_2_0) /\ _r_2(x_1_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)) <= _r_2(x_1_0, 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_4(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) /\ _r_3(x_0_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_1(x_0_1, x_2_0) /\ _r_4(x_2_0) append(cons(x_0_0, x_0_1), nil, cons(x_2_0, x_2_1)) <= _r_2(x_0_0, x_2_1) /\ _r_4(x_0_0) /\ _r_4(x_2_0) append(nil, cons(x_1_0, x_1_1), cons(x_2_0, x_2_1)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_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 } ] -- Equality automata are defined for: {nat, natlist} _|