[Enter formulas separated by commas (e.g. 'Pa, Pa then Qb, Rca')]
[You can use '¬'/'not', 'and'/'&', 'or', 'then', 'iff', '°', "all"/"V", "exists"/"E"
for negation, conjunction, disjunction, conditional, biconditional, consistency and the quantifiers]
[Acceptable individual constants are: 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l', 'm', 'n']
[Acceptable predicate letters are: 'P', 'Q', 'R', 'S', 'T', 'U', 'A', 'B', 'C']
[Acceptable variables are: 'u', 'v', 'w', 'x', 'y', 'z']
[For the accepted model input format see the solution to the first preset excercise]
WARNING: This module will not check if set of sentences you entered has a finite model such that the
sentences all get the desired value
WARNING: The solving algorithm is heuristic and it may not find a solution even if the model sought exists