[Enter premises separated by commas and conclusion separated with / (e.g. 'Pa, Pa then Qb / Qb')]
[You can use '¬'/'not', 'and'/'&', 'or', 'then', "all"/"V", "exists"/"E" for negation, conjunction, disjunction, conditional, and the quantifiers]
[Use 'Falsum' for the '⊥' symbol]
[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']
[On steps are separated with commas (e.g. "1, 2"), except for I¬ and I→ rules, which use a slash (e.g "1-4")]
WARNING: This module will not check if the argument you entered is valid
WARNING: The solving algorithm is heuristic and it may not find a solution even if the argument is valid

---