qcheck_runner_log

random seed: 92577147
law dummy_fail: 1 relevant cases (1 total)
  test `dummy_fail`
  failed on ≥ 1 cases:
  ⟦∀ v0 : list(a), v1 : list(a), v2 : list(a), v3 : list(a), v4 : list(a), v5 : list(a), v6 : list(a), v7 : list(a), v8 : list(a), v9 : list(a), v0 : a, v1 : a, v2 : a, v3 : a, v4 : a, v5 : a, v6 : a, v7 : a, v8 : a, v9 : a, v0 : b, v1 : b, v2 : b, v4 : b, v5 : b, v6 : b, v7 : b, v9 : b, v0 : pair(a, b), v1 : pair(a, b), v5 : pair(a, b). f_p(h_a(cons(a; h_a(cons(a; g_a(h_a(cons(a; g_a(f_a(h_a(cons(a; h_a(cons(a; f_a(h_a(cons(a; g_a(f_a(g_a(h_a(nil(a; )), b_0)), g_b(h_b(pair(a, b; h_a(cons(a; g_a(a_1, b_1), v3)), h_b(pair(a, b; g_a(a_1, b_1), h_b(pair(a, b; v3, g_b(h_b(pair(a, b; v4, g_b(v0, a_2))), a_1))))))), f_a(f_a(f_a(h_a(cons(a; h_a(cons(a; f_a(a_2), v1)), v3))))))), nil(a; )))), cons(a; v9, nil(a; )))), cons(a; a_0, cons(a; v8, cons(a; f_a(h_a(cons(a; f_a(g_a(f_a(a_0), b_0)), v9))), cons(a; h_a(cons(a; h_a(v1), nil(a; ))), cons(a; f_a(a_1), v6)))))))), h_b(pair(a, b; f_a(a_0), h_b(pair(a, b; a_2, g_b(b_2, f_a(f_a(a_2)))))))), cons(a; a_2, cons(a; g_a(g_a(f_a(a_1), g_b(h_b(pair(a, b; a_0, b_2)), a_0)), f_b(h_b(pair(a, b; v9, b_0)))), cons(a; g_a(v0, b_0), nil(a; )))))), f_b(f_b(f_b(h_b(pair(a, b; h_a(cons(a; g_a(a_2, h_b(pair(a, b; f_a(v9), h_b(pair(a, b; a_1, b_2))))), cons(a; g_a(a_1, g_b(v2, f_a(f_a(f_a(a_1))))), cons(a; h_a(cons(a; g_a(a_2, b_2), cons(a; v2, v6))), cons(a; h_a(cons(a; a_0, nil(a; ))), cons(a; v4, cons(a; a_0, v9))))))), f_b(f_b(f_b(h_b(pair(a, b; g_a(h_a(cons(a; g_a(v7, h_b(pair(a, b; a_2, b_1))), cons(a; a_0, nil(a; )))), g_b(h_b(pair(a, b; f_a(h_a(cons(a; a_1, v0))), b_1)), f_a(g_a(g_a(a_2, h_b(pair(a, b; a_1, b_1))), h_b(pair(a, b; h_a(cons(a; a_2, v5)), h_b(v1))))))), g_b(b_1, h_a(cons(a; v8, cons(a; v3, cons(a; v2, cons(a; v8, v7))))))))))))))))), cons(a; a_0, cons(a; h_a(cons(a; g_a(f_a(g_a(f_a(a_1), b_2)), g_b(b_1, h_a(cons(a; h_a(cons(a; v9, v6)), nil(a; ))))), nil(a; ))), cons(a; h_a(cons(a; f_a(h_a(cons(a; f_a(g_a(f_a(h_a(cons(a; f_a(h_a(v4)), nil(a; )))), b_0)), cons(a; g_a(v3, v5), cons(a; f_a(a_1), v5))))), cons(a; g_a(v8, b_0), cons(a; a_2, cons(a; v7, cons(a; a_0, nil(a; ))))))), cons(a; g_a(h_a(cons(a; g_a(a_0, v1), nil(a; ))), h_b(v5)), v3)))))), cons(a; f_a(g_a(h_a(cons(a; a_0, v6)), h_b(v0))), cons(a; h_a(cons(a; g_a(h_a(cons(a; g_a(a_1, v9), cons(a; g_a(f_a(a_2), v6), v6))), f_b(h_b(pair(a, b; g_a(a_1, f_b(f_b(f_b(h_b(pair(a, b; g_a(a_1, b_0), b_2)))))), b_2)))), cons(a; a_0, nil(a; )))), cons(a; a_1, cons(a; f_a(g_a(a_1, v6)), cons(a; f_a(h_a(cons(a; v9, nil(a; )))), nil(a; )))))))), f_b(f_b(f_b(g_b(f_b(f_b(h_b(pair(a, b; h_a(cons(a; g_a(g_a(a_0, h_b(pair(a, b; g_a(a_0, b_0), f_b(g_b(b_0, v2))))), g_b(g_b(h_b(pair(a, b; h_a(cons(a; v2, nil(a; ))), b_0)), v2), f_a(g_a(a_0, g_b(f_b(g_b(b_1, a_2)), f_a(h_a(cons(a; g_a(f_a(a_1), g_b(v7, a_0)), v4)))))))), v4)), h_b(pair(a, b; g_a(g_a(f_a(f_a(f_a(g_a(a_1, b_2)))), h_b(pair(a, b; g_a(f_a(f_a(h_a(nil(a; )))), b_0), h_b(pair(a, b; h_a(cons(a; a_0, v7)), f_b(v5)))))), f_b(f_b(b_2))), h_b(pair(a, b; f_a(g_a(f_a(f_a(f_a(h_a(cons(a; h_a(cons(a; h_a(cons(a; a_2, cons(a; a_2, nil(a; )))), cons(a; g_a(f_a(v3), b_2), cons(a; v5, v8)))), cons(a; v8, cons(a; a_1, v1))))))), h_b(pair(a, b; h_a(cons(a; a_0, cons(a; a_0, cons(a; f_a(v2), cons(a; a_0, cons(a; a_1, nil(a; ))))))), b_1)))), h_b(pair(a, b; g_a(f_a(a_2), f_b(h_b(pair(a, b; v0, b_2)))), f_b(h_b(pair(a, b; v9, v2))))))))))))), g_a(f_a(f_a(g_a(f_a(g_a(h_a(cons(a; h_a(cons(a; h_a(v7), cons(a; f_a(a_2), v1))), cons(a; h_a(cons(a; a_2, v4)), nil(a; )))), f_b(h_b(pair(a, b; h_a(nil(a; )), g_b(b_0, g_a(g_a(h_a(v4), b_1), v0))))))), h_b(pair(a, b; f_a(g_a(g_a(g_a(v7, v4), g_b(h_b(pair(a, b; h_a(nil(a; )), h_b(pair(a, b; a_2, b_2)))), v5)), f_b(f_b(g_b(g_b(f_b(h_b(pair(a, b; a_2, b_2))), a_1), f_a(g_a(a_0, g_b(b_2, v1)))))))), f_b(h_b(pair(a, b; h_a(v6), g_b(h_b(pair(a, b; a_1, b_1)), f_a(f_a(f_a(a_0)))))))))))), f_b(g_b(h_b(pair(a, b; g_a(f_a(g_a(h_a(cons(a; g_a(a_2, b_2), cons(a; v5, v4))), h_b(pair(a, b; v1, b_0)))), g_b(v7, a_2)), h_b(pair(a, b; h_a(cons(a; h_a(cons(a; h_a(cons(a; h_a(cons(a; a_1, cons(a; h_a(cons(a; a_1, v6)), nil(a; )))), cons(a; v0, v1))), cons(a; g_a(a_1, b_1), v3))), cons(a; f_a(g_a(h_a(cons(a; a_2, cons(a; a_1, cons(a; a_2, v2)))), h_b(pair(a, b; f_a(f_a(h_a(cons(a; v9, cons(a; v2, v0))))), b_1)))), cons(a; h_a(cons(a; a_2, cons(a; f_a(g_a(f_a(a_0), b_2)), v0))), cons(a; v9, cons(a; a_1, cons(a; g_a(h_a(cons(a; f_a(a_2), cons(a; a_0, nil(a; )))), b_2), nil(a; )))))))), f_b(h_b(pair(a, b; g_a(g_a(g_a(f_a(f_a(h_a(cons(a; a_0, v0)))), g_b(f_b(b_2), a_2)), g_b(g_b(g_b(b_1, v1), v4), f_a(h_a(cons(a; a_1, v4))))), f_b(g_b(b_2, g_a(f_a(h_a(cons(a; v5, nil(a; )))), f_b(g_b(f_b(f_b(f_b(b_0))), h_a(cons(a; g_a(f_a(a_2), g_b(v7, g_a(a_2, v7))), v9)))))))), h_b(pair(a, b; f_a(h_a(cons(a; g_a(h_a(cons(a; f_a(a_0), v7)), h_b(pair(a, b; v0, h_b(pair(a, b; g_a(a_1, b_1), b_2))))), cons(a; a_1, cons(a; a_2, v4))))), h_b(pair(a, b; g_a(g_a(f_a(v0), v1), f_b(f_b(h_b(pair(a, b; h_a(cons(a; v2, v6)), h_b(pair(a, b; a_1, b_1))))))), h_b(pair(a, b; v3, f_b(g_b(b_0, h_a(nil(a; ))))))))))))))))), f_a(h_a(cons(a; f_a(f_a(g_a(g_a(f_a(g_a(f_a(g_a(f_a(v5), h_b(pair(a, b; h_a(nil(a; )), b_1)))), g_b(f_b(b_2), a_0))), g_b(b_0, a_2)), h_b(pair(a, b; f_a(f_a(v5)), g_b(b_2, g_a(a_1, b_0))))))), cons(a; h_a(cons(a; h_a(nil(a; )), cons(a; v2, v0))), cons(a; h_a(cons(a; g_a(f_a(v0), f_b(h_b(pair(a, b; a_1, f_b(h_b(pair(a, b; a_0, b_0))))))), cons(a; v6, v9))), cons(a; a_2, nil(a; )))))))))))))))⟧
  
law dummy_error: 0 relevant cases (1 total)
  test `dummy_error` raised exception `Not_found`
on `a_1 (after 5 shrink steps)`
law fixpoint_occur: 100 relevant cases (122 total)
law fixpoint_is_proj: 100 relevant cases (128 total)
law match_subst: 23 relevant cases (230 total)
law subst_match: 100 relevant cases (126 total)
law robinson_subst: 10 relevant cases (71 total)
law subst_robinson: 100 relevant cases (136 total)
law naive_correct_match: 10 relevant cases (10 total)
law naive_correct_unify: 10 relevant cases (10 total)
law index_correct_match: 10 relevant cases (10 total)
law index_correct_unify: 10 relevant cases (10 total)
law fingerprint_correct_match: 10 relevant cases (10 total)
law fingerprint_correct_unify: 10 relevant cases (10 total)
law index_complete_match: 10 relevant cases (10 total)
law index_complete_unify: 10 relevant cases (10 total)
law fingerprint_complete_match: 10 relevant cases (10 total)
law fingerprint_complete_unify: 10 relevant cases (10 total)
failure (2 tests failed, ran 18 tests)