Een formule invoeren doe je met de knop <=]. CL verwijdert een formule, en met < kan je terugwaarts per symbool verwijderen (als <=] nog niet gebruikt is.Indien je dat al wel gedaan hebt, gebruik in dat geval CL).
Als je formule gesloten is (geen vrije variabelen), dan berekent de machine domweg de waarheidswaarde op het model. Tenslotte hangt de waarheidswaarde van zo'n
gesloten formule niet af van de assignments. Als de formule waar is dan gaat het groene lampje branden, als hij onwaar is gaat het rode lampje branden.
Interessantere resultaten geven 'echte queries', een ondervraging van de database met formules met vrije variabelen. Onder de knop POS worden dan een positieve instantie gegeven (assignments voor de vrije variabelen die de formule waarmaken), en onder NEG een tegenvoorbeeld (assignments voor de vrije variabelen die de formule onwaar maken). Door op POS en NEG te drukken kan je volgende instanties genereren (indien die voor handen zijn). Als POS en NEG allebei resultaten hebben, dan gaat het oranje lampje branden. Indien er slechts positieve instanties zijn, dan is de formule (ondanks de aanwezigheid van vrije variabelen) waar en gaat de groene lamp branden. Een simpel voorbeeld is Fx v Mx. In het geval er slechts negatieve instanties zijn, dan gaat de rode lamp branden: de formule is onwaar ongeacht de assignment van de vrije variabelen.