fof(f1, axiom,
  ~ hBOOL(c_fFalse)
).

fof(f2, axiom,
  hBOOL(c_fTrue)
).

fof(f3, axiom,
  ![V_y, V_ys] :
    (c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_y, V_ys)) =
    c_Nat_OSuc(c_Nat_Osize__class_Osize(V_ys)))
).

fof(f4, axiom,
  ![V_xs, V_n] :
    ((~ (c_Nat_Osize__class_Osize(V_xs) = c_Nat_OSuc(V_n))) |
    (c_Nat_Osize__class_Osize(c_ATP_OSkoo_O6_O0_O1(V_n,V_xs)) = V_n))
).

fof(f5, axiom,
  ![V_xs, V_n] :
    ((~ (c_Nat_Osize__class_Osize(V_xs) = c_Nat_OSuc(V_n))) |
     (V_xs = c_List_Olist_OCons(c_ATP_OSkoo_O6_O1_O1(V_n, V_xs), c_ATP_OSkoo_O6_O0_O1(V_n, V_xs))))
).

fof(f6, axiom,
  c_Nat_Osize__class_Osize(c_List_Olist_ONil) = c_Groups_Ozero__class_Ozero
).

fof(f7, axiom,
  ![V_xs] :
    ((~ (c_Nat_Osize__class_Osize(V_xs) = c_Groups_Ozero__class_Ozero)) |
    (V_xs = c_List_Olist_ONil))
).

fof(f8, axiom,
  ~ (v_p = c_List_Olist_ONil)
).