; user defined axiom: 
(assert (forall ((l1_s0 Bool))
    true))