Solving ../../benchmarks/smtlib/true/prefix_count.smt2... Inference procedure has parameters: Ice fuel: 200 Timeout: Some(60.) (sec) Teacher_type: Checks all clauses every time Approximation method: remove every clause that can be safely removed Learning problem is: env: { elt -> {a, b} ; eltlist -> {cons, nil} ; nat -> {s, z} } definition: { (leq, P: { leq(z, s(nn2)) <= True leq(z, z) <= True leq(s(nn1), s(nn2)) <= leq(nn1, nn2) leq(nn1, nn2) <= leq(s(nn1), s(nn2)) False <= leq(s(nn1), z) } ) (prefix, P: { prefix(nil, y) <= True prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) eq_elt(z, y2) <= prefix(cons(z, zs), cons(y2, ys)) False <= prefix(cons(z, zs), nil) } ) (count, F: { count(x, nil, z) <= True count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) } eq_nat(_qs, _rs) <= count(_os, _ps, _qs) /\ count(_os, _ps, _rs) ) } properties: { leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) } over-approximation: {count, prefix} under-approximation: {leq} Clause system for inference is: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Solving took 60.170958 seconds. Maybe: timeout during learnerLast solver state: Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, cons(a, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(a, nil)), z) /\ prefix(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= count(a, cons(b, cons(b, nil)), s(z)) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) count(b, cons(b, cons(b, cons(b, nil))), s(s(z))) <= count(b, cons(b, cons(b, nil)), s(z)) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) prefix(cons(b, nil), nil) <= prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) prefix(cons(a, nil), cons(b, cons(a, nil))) <= prefix(cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, cons(a, nil)), nil) prefix(cons(b, cons(a, nil)), cons(a, nil)) <= prefix(cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= _r_6(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_1) /\ _r_6(x_0_0) /\ _r_6(x_1_0) prefix(cons(x_0_0, x_0_1), nil) <= _r_5(x_0_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| ------------------- STEPS: ------------------------------------------- Step 0, which took 0.005834 s (model generation: 0.005743, model checking: 0.000091): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { } Current best model: |_ name: None count -> [ count : { } ] ; leq -> [ leq : { } ] ; prefix -> [ prefix : { } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : Yes: { x -> b } prefix(nil, y) <= True : Yes: { y -> nil } leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : No: () count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 1, which took 0.005878 s (model generation: 0.005785, model checking: 0.000093): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(b, nil, z) <= True prefix(nil, nil) <= True } Current best model: |_ name: None count -> [ count : { count(b, nil, z) <= True } ] ; leq -> [ leq : { } ] ; prefix -> [ prefix : { prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : Yes: { x -> a } prefix(nil, y) <= True : Yes: { y -> cons(_bcuba_0, _bcuba_1) } leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> z ; _ts -> z ; l1 -> nil ; l2 -> nil ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> z ; t1 -> nil ; x -> b } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> z ; h1 -> a ; t1 -> nil ; x -> b } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { ys -> nil ; zs -> nil } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 2, which took 0.013457 s (model generation: 0.013274, model checking: 0.000183): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True } Current best model: |_ name: None count -> [ count : { count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> z ; _ts -> s(_gduba_0) ; l1 -> nil ; l2 -> cons(_iduba_0, _iduba_1) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> z ; t1 -> nil ; x -> a } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> z ; h1 -> b ; t1 -> nil ; x -> a } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : Yes: { nn1 -> z ; nn2 -> z } leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : Yes: { ys -> nil ; zs -> cons(_uduba_0, _uduba_1) } ------------------------------------------- Step 3, which took 0.015494 s (model generation: 0.015385, model checking: 0.000109): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True leq(z, s(z)) <= count(b, cons(a, nil), s(z)) prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= True leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True prefix(cons(x_0_0, x_0_1), nil) <= True prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(_vduba_0) ; _ts -> z ; l1 -> cons(_xduba_0, _xduba_1) ; l2 -> cons(_yduba_0, _yduba_1) ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : Yes: { nn1 -> s(_peuba_0) ; nn2 -> z } False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 4, which took 0.013066 s (model generation: 0.012914, model checking: 0.000152): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True leq(s(z), z) <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) leq(s(z), z) <= leq(s(s(z)), s(z)) prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= True count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= True leq(s(x_0_0), z) <= True leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True prefix(cons(x_0_0, x_0_1), nil) <= True prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : No: () count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : Yes: { } prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 5, which took 0.026373 s (model generation: 0.026208, model checking: 0.000165): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= _r_1(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True prefix(cons(x_0_0, x_0_1), nil) <= True prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(_qfuba_0) ; _ts -> z ; l1 -> cons(_sfuba_0, _sfuba_1) ; l2 -> nil ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 6, which took 0.013539 s (model generation: 0.013307, model checking: 0.000232): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) False <= count(b, cons(a, nil), s(z)) /\ prefix(cons(a, nil), nil) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) prefix(cons(a, nil), nil) <= prefix(cons(a, cons(a, nil)), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= _r_1(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= True prefix(cons(x_0_0, x_0_1), nil) <= True prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(_xguba_0) ; _ts -> z ; l1 -> cons(_zguba_0, _zguba_1) ; l2 -> nil ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> s(_iiuba_0) ; h1 -> a ; t1 -> cons(b, _kiuba_1) ; x -> b } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 7, which took 0.015254 s (model generation: 0.014863, model checking: 0.000391): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), nil) } Current best model: |_ name: None count -> [ count : { _r_1(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(a, cons(x_1_0, x_1_1), z) <= _r_1(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(s(_aluba_0)) ; _ts -> s(z) ; l1 -> cons(_ziuba_0, nil) ; l2 -> cons(_ajuba_0, nil) ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 8, which took 0.032388 s (model generation: 0.031997, model checking: 0.000391): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), nil) } Current best model: |_ name: None count -> [ count : { _r_1(z) <= True _r_2(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_2(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= True count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { _r_1(z) <= True leq(s(x_0_0), s(x_1_0)) <= _r_1(x_0_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(s(_xnuba_0)) ; _ts -> s(_zluba_0) ; l1 -> cons(_amuba_0, nil) ; l2 -> cons(_bmuba_0, nil) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> s(z) ; t1 -> cons(_jmuba_0, _jmuba_1) ; x -> a } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : Yes: { nn1 -> s(z) ; nn2 -> s(_enuba_0) } leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 9, which took 0.027947 s (model generation: 0.027572, model checking: 0.000375): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(b, cons(a, nil), s(s(z))) /\ count(b, cons(a, nil), s(z)) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), nil) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_2(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(_zouba_0, nil) ; l2 -> cons(b, nil) ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 10, which took 0.047433 s (model generation: 0.047074, model checking: 0.000359): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(b, cons(a, nil), s(s(z))) /\ count(b, cons(a, nil), s(z)) leq(z, s(z)) <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_3(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_2(nil, a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(_ctuba_0, nil) ; l2 -> cons(a, _dtuba_1) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { y2 -> b ; ys -> nil ; zs -> nil } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 11, which took 0.090136 s (model generation: 0.089260, model checking: 0.000876): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(nil, z) <= True _r_4(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_4(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(nil, a) <= True _r_4(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1, x_1_0) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> z ; _ts -> s(z) ; l1 -> nil ; l2 -> cons(_aavba_0, cons(_qdvba_0, _qdvba_1)) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> z ; t1 -> cons(b, _lavba_1) ; x -> a } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> s(z) ; h1 -> b ; t1 -> cons(_qbvba_0, nil) ; x -> a } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { y2 -> a ; ys -> cons(_cdvba_0, _cdvba_1) ; zs -> cons(b, _ddvba_1) } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : Yes: { y2 -> b ; ys -> nil ; zs -> cons(_pdvba_0, _pdvba_1) } ------------------------------------------- Step 12, which took 0.167227 s (model generation: 0.166283, model checking: 0.000944): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) prefix(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_2(nil, z) <= True _r_4(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_4(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(a, a) <= True _r_3(b, b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(b, cons(b, nil)) ; l2 -> cons(b, cons(b, nil)) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 13, which took 0.181316 s (model generation: 0.179344, model checking: 0.001972): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) prefix(cons(a, cons(b, nil)), cons(a, cons(a, nil))) <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= True _r_2(nil, z) <= True _r_3(b) <= True _r_4(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(b) <= True _r_4(a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(_grvba_0) ; _ts -> z ; l1 -> cons(b, nil) ; l2 -> cons(a, nil) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 14, which took 0.131762 s (model generation: 0.120916, model checking: 0.010846): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(b) <= True _r_4(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(b) <= True _r_4(a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(s(_jpwba_0)) ; _ts -> s(z) ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 15, which took 0.126728 s (model generation: 0.115209, model checking: 0.011519): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= count(b, cons(b, nil), s(s(z))) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(a) <= True _r_4(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(a) <= True _r_4(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(b, cons(b, nil)) ; l2 -> cons(b, cons(b, nil)) ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> z ; t1 -> cons(_fdyba_0, _fdyba_1) ; x -> b } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> s(s(_kxyba_0)) ; h1 -> a ; t1 -> cons(b, cons(_jxyba_0, _jxyba_1)) ; x -> b } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 16, which took 0.182096 s (model generation: 0.170426, model checking: 0.011670): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) /\ count(a, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= count(b, cons(b, nil), s(s(z))) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= _r_3(x_0_0) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(a) <= True _r_4(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) /\ _r_3(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(a) <= True _r_4(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0) /\ _r_3(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(a, cons(a, nil)) ; l2 -> cons(a, cons(a, nil)) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> s(z) ; h1 -> b ; t1 -> cons(b, nil) ; x -> a } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 17, which took 0.381821 s (model generation: 0.380824, model checking: 0.000997): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) /\ count(a, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) count(a, cons(b, cons(b, nil)), s(z)) <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(a, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= count(b, cons(b, nil), s(s(z))) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= True count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(a, a) <= True _r_3(b, b) <= True _r_4(nil) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_0, x_1_0) /\ _r_4(x_0_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(b, nil) ; l2 -> cons(b, _arbca_1) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { ys -> cons(b, _tubca_1) ; zs -> cons(b, nil) } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 18, which took 0.512294 s (model generation: 0.500953, model checking: 0.011341): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) /\ count(a, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) count(a, cons(b, cons(b, nil)), s(z)) <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(a, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(z) <= True _r_2(nil) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(a) <= True _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= _r_2(x_1_1) /\ _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= _r_2(x_1_1) /\ _r_4(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_4(a) <= True _r_5(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(b, nil) ; l2 -> cons(b, nil) ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> z ; h1 -> b ; t1 -> cons(b, nil) ; x -> a } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 19, which took 0.480331 s (model generation: 0.478295, model checking: 0.002036): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(a, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) /\ prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_4(a) <= True _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_3(cons(x_0_0, x_0_1), a) <= _r_5(x_0_0) _r_3(nil, a) <= True _r_3(nil, b) <= True _r_4(a) <= True _r_5(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1, x_1_0) /\ _r_4(x_0_0) /\ _r_4(x_1_0) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_3(x_0_1, x_1_0) /\ _r_5(x_0_0) /\ _r_5(x_1_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(s(_afeca_0)) ; _ts -> z ; l1 -> cons(a, cons(b, _zeeca_1)) ; l2 -> cons(a, _tvdca_1) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { y2 -> b ; ys -> cons(b, _eaeca_1) ; zs -> cons(b, nil) } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : Yes: { y2 -> a ; ys -> nil ; zs -> cons(b, _heeca_1) } ------------------------------------------- Step 20, which took 0.579908 s (model generation: 0.577201, model checking: 0.002707): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(a, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) leq(s(s(z)), z) <= count(b, cons(a, cons(b, nil)), s(s(z))) /\ prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) prefix(cons(b, nil), nil) <= prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), s(x_1_0)) <= True _r_1(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) _r_1(nil, z) <= True _r_3(cons(x_0_0, x_0_1)) <= True _r_4(a) <= True _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_3(x_1_1) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) /\ _r_4(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_2(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_1_0) _r_2(nil, nil) <= True _r_4(a) <= True _r_5(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_1) /\ _r_4(x_0_0) /\ _r_4(x_1_0) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_2(x_0_1, x_1_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(_bmeca_0) ; _ts -> z ; l1 -> cons(a, cons(_kyeca_0, _kyeca_1)) ; l2 -> cons(a, cons(b, _lyeca_1)) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> s(z) ; h1 -> b ; t1 -> cons(b, cons(a, _nyeca_1)) ; x -> a } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { ys -> cons(_hteca_0, _hteca_1) ; zs -> nil } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : Yes: { y2 -> b ; ys -> cons(b, cons(_txeca_0, _txeca_1)) ; zs -> cons(_aweca_0, nil) } ------------------------------------------- Step 21, which took 0.853330 s (model generation: 0.841180, model checking: 0.012150): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, cons(a, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(a, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(b, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) leq(s(s(z)), z) <= count(b, cons(a, cons(b, nil)), s(s(z))) /\ prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) prefix(cons(b, nil), nil) <= prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) prefix(cons(a, nil), cons(b, cons(a, nil))) <= prefix(cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= _r_2(x_0_1) _r_1(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1)) <= True _r_3(nil) <= True _r_4(a) <= True _r_5(b) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_2(x_1_1) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1) /\ _r_4(x_1_0) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= _r_3(x_1_1) /\ _r_4(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_4(a) <= True _r_5(b) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(s(_crfca_0)) ; _ts -> s(z) ; l1 -> cons(a, cons(b, nil)) ; l2 -> cons(a, cons(b, nil)) ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : No: () eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> z ; h1 -> a ; t1 -> cons(a, nil) ; x -> b } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 22, which took 1.179059 s (model generation: 1.167289, model checking: 0.011770): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, cons(a, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(b, nil)), s(z)) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(b, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) prefix(cons(b, nil), nil) <= prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) prefix(cons(a, nil), cons(b, cons(a, nil))) <= prefix(cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), z) <= _r_4(x_0_0) _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(b) <= True _r_5(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= _r_4(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_4(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_4(b) <= True _r_5(a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_0) /\ _r_4(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_5(x_0_0) /\ _r_5(x_1_0) /\ prefix(x_0_1, x_1_1) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(_pchca_0) ; _ts -> z ; l1 -> cons(b, cons(a, nil)) ; l2 -> cons(b, cons(a, nil)) ; x -> a } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> s(z) ; t1 -> cons(_jghca_0, cons(b, _zjica_1)) ; x -> b } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : Yes: { _ns -> s(z) ; h1 -> a ; t1 -> cons(a, cons(b, _bthca_1)) ; x -> b } leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : No: () prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : No: () ------------------------------------------- Step 23, which took 54.072288 s (model generation: 54.069789, model checking: 0.002499): Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, cons(a, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(a, nil)), z) /\ prefix(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= count(a, cons(b, cons(b, nil)), s(z)) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ count(b, cons(a, cons(b, nil)), z) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(b, nil))) False <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) leq(z, s(z)) <= count(b, cons(a, cons(a, nil)), s(z)) /\ prefix(nil, cons(a, cons(a, nil))) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) prefix(cons(b, nil), nil) <= prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) prefix(cons(a, nil), cons(b, cons(a, nil))) <= prefix(cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= _r_6(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_1) /\ _r_6(x_0_0) /\ _r_6(x_1_0) prefix(cons(x_0_0, x_0_1), nil) <= _r_5(x_0_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _| Answer of teacher: count(x, nil, z) <= True : No: () prefix(nil, y) <= True : No: () leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) : Yes: { _ss -> s(z) ; _ts -> z ; l1 -> cons(b, cons(_npjca_0, _npjca_1)) ; l2 -> nil ; x -> b } count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) : Yes: { _ms -> s(z) ; t1 -> cons(b, cons(b, nil)) ; x -> b } eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) : No: () leq(s(nn1), s(nn2)) <= leq(nn1, nn2) : No: () leq(nn1, nn2) <= leq(s(nn1), s(nn2)) : No: () False <= leq(s(nn1), z) : No: () prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) : Yes: { ys -> cons(a, _ykjca_1) ; zs -> cons(a, nil) } prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) : Yes: { y2 -> b ; ys -> cons(a, _wnjca_1) ; zs -> cons(b, cons(a, _ypjca_1)) } Total time: 60.170958 Learner time: 59.071091 Teacher time: 0.083868 Reasons for stopping: Maybe: timeout during learnerLast solver state: Clauses: { count(x, nil, z) <= True -> 0 prefix(nil, y) <= True -> 0 leq(_ss, _ts) <= count(x, l1, _ss) /\ count(x, l2, _ts) /\ prefix(l1, l2) -> 0 count(x, cons(x, t1), s(_ms)) <= count(x, t1, _ms) -> 0 eq_elt(h1, x) \/ count(x, cons(h1, t1), _ns) <= count(x, t1, _ns) -> 0 leq(s(nn1), s(nn2)) <= leq(nn1, nn2) -> 0 leq(nn1, nn2) <= leq(s(nn1), s(nn2)) -> 0 False <= leq(s(nn1), z) -> 0 prefix(cons(y2, zs), cons(y2, ys)) <= prefix(zs, ys) -> 0 prefix(zs, ys) <= prefix(cons(y2, zs), cons(y2, ys)) -> 0 } Accumulated learning constraints: { count(a, cons(a, cons(a, nil)), s(s(z))) <= True count(a, cons(a, cons(b, nil)), s(z)) <= True count(a, cons(a, nil), s(z)) <= True count(a, cons(b, cons(a, nil)), s(z)) <= True count(a, cons(b, cons(b, cons(a, nil))), s(z)) <= True count(a, cons(b, cons(b, nil)), z) <= True count(a, cons(b, nil), z) <= True count(a, nil, z) <= True count(b, cons(a, cons(a, cons(b, nil))), s(z)) <= True count(b, cons(a, cons(a, nil)), z) <= True count(b, cons(a, cons(b, nil)), s(z)) <= True count(b, cons(a, nil), z) <= True count(b, cons(b, cons(a, cons(b, nil))), s(s(z))) <= True count(b, cons(b, cons(a, nil)), s(z)) <= True count(b, cons(b, nil), s(z)) <= True count(b, nil, z) <= True leq(s(s(z)), s(s(z))) <= True leq(s(z), s(z)) <= True leq(z, z) <= True prefix(cons(a, cons(a, nil)), cons(a, cons(a, nil))) <= True prefix(cons(a, cons(b, nil)), cons(a, cons(b, nil))) <= True prefix(cons(a, nil), cons(a, cons(a, nil))) <= True prefix(cons(a, nil), cons(a, nil)) <= True prefix(cons(b, cons(b, nil)), cons(b, cons(b, nil))) <= True prefix(cons(b, nil), cons(b, nil)) <= True prefix(nil, cons(a, nil)) <= True prefix(nil, nil) <= True False <= count(a, cons(a, nil), s(s(z))) False <= count(a, cons(a, nil), z) False <= count(a, cons(b, cons(a, nil)), z) /\ prefix(cons(b, cons(a, nil)), cons(b, cons(a, nil))) False <= count(a, cons(b, cons(b, nil)), s(z)) False <= count(a, cons(b, nil), s(z)) False <= count(b, cons(a, cons(a, nil)), s(z)) False <= count(b, cons(a, cons(b, nil)), s(s(z))) False <= count(b, cons(a, nil), s(z)) count(b, cons(a, cons(b, cons(a, nil))), s(s(z))) <= count(b, cons(b, cons(a, nil)), s(s(z))) count(b, cons(b, cons(b, cons(b, nil))), s(s(z))) <= count(b, cons(b, cons(b, nil)), s(z)) False <= count(b, cons(b, cons(b, nil)), s(z)) /\ count(b, cons(b, cons(b, nil)), z) False <= count(b, cons(b, nil), s(s(z))) False <= count(b, cons(b, nil), z) False <= leq(s(s(z)), s(z)) False <= leq(s(z), z) False <= prefix(cons(a, cons(a, nil)), cons(a, nil)) prefix(cons(b, nil), nil) <= prefix(cons(a, cons(b, nil)), cons(a, nil)) False <= prefix(cons(a, nil), cons(b, nil)) False <= prefix(cons(a, nil), nil) prefix(cons(a, nil), cons(b, cons(a, nil))) <= prefix(cons(b, cons(a, nil)), cons(b, cons(b, cons(a, nil)))) False <= prefix(cons(b, cons(a, nil)), cons(b, nil)) False <= prefix(cons(b, cons(a, nil)), nil) prefix(cons(b, cons(a, nil)), cons(a, nil)) <= prefix(cons(b, cons(b, cons(a, nil))), cons(b, cons(a, nil))) False <= prefix(cons(b, nil), cons(a, nil)) } Current best model: |_ name: None count -> [ count : { _r_1(cons(x_0_0, x_0_1), z) <= True _r_1(nil, z) <= True _r_2(cons(x_0_0, x_0_1), z) <= True _r_3(cons(x_0_0, x_0_1)) <= _r_3(x_0_1) _r_3(cons(x_0_0, x_0_1)) <= _r_6(x_0_0) _r_5(b) <= True _r_6(a) <= True count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_6(x_1_0) count(a, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(a, cons(x_1_0, x_1_1), z) <= _r_5(x_1_0) count(a, nil, z) <= True count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_1(x_1_1, x_2_0) /\ _r_5(x_1_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_2(x_1_1, x_2_0) count(b, cons(x_1_0, x_1_1), s(x_2_0)) <= _r_3(x_1_1) count(b, cons(x_1_0, x_1_1), z) <= _r_6(x_1_0) count(b, nil, z) <= True } ] ; leq -> [ leq : { leq(s(x_0_0), s(x_1_0)) <= leq(x_0_0, x_1_0) leq(z, s(x_1_0)) <= True leq(z, z) <= True } ] ; prefix -> [ prefix : { _r_4(cons(x_0_0, x_0_1)) <= _r_5(x_0_0) _r_4(nil) <= True _r_5(b) <= True _r_6(a) <= True prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_1) /\ _r_5(x_0_0) /\ _r_5(x_1_0) prefix(cons(x_0_0, x_0_1), cons(x_1_0, x_1_1)) <= _r_4(x_0_1) /\ _r_6(x_0_0) /\ _r_6(x_1_0) prefix(cons(x_0_0, x_0_1), nil) <= _r_5(x_0_0) prefix(nil, cons(x_1_0, x_1_1)) <= True prefix(nil, nil) <= True } ] -- Equality automata are defined for: {elt, eltlist, nat} _|