// A vocabulary defines types and signatures of functions and predicates.
vocabulary MyVocabulary {
    // For classical first-order logic, a single type T is sufficient.
    type T
    
    // All predicates must be listed here:
    R(T,T)        // R is a predicate of arity 2
    S(T)          // S is a predicate of arity 1
    
    // All functions must be listed here:
    f(T) : T     // f is a function of arity 1
    c : T        // c is a function of arity 0
    d : T        // d is a function of arity 0
}

// A theory consists of a set of well formed formulas.
// Each formula is terminated by full stop.
// Symbols are pretty-printed:
//  - conjunction: &
//  - disjunction: |
//  - implication: =>
//  - equivalence: <=>
//  - negation:    ~
//  - for all:     !
//  - exists:      ?
// Quantifiers are followed by a space-separated list of variables. After that, there is a semicolon and the subformula on which the quantifiers are applied.
theory MyTheory : MyVocabulary {
    !x y z: R(x,y) | R(z,c) | S(z).
    !u v w: ~R(f(u),u) | ~R(v,w).
    ~S(f(d)).
}

// Here we define a partial structure. For our purposes, we only specify the domain of T.
structure MyStructure : MyVocabulary {
    T = {0..1}
}

// This is the entry point. For our purposes, we can leave it as it is.
procedure main() {
    printmodels(modelexpand(MyTheory, MyStructure))
}