> FORMULA: (False | G True) & (F False | True)

> MATHSAT:
k: 0
k-unraveling: (False | (True & <X G True,0>)) & (False | <X F False,0> | True)
empty: True & !<X F False,0> & !<X G True,0>
loop: False
empty or loop: (True & !<X F False,0> & !<X G True,0>) | False
prune: False

k: 1
k-unraveling: True & (<X G True,0> <-> (True & <X G True,1>)) & (<X F False,0> <-> (False | <X F False,1>))
empty: True & !<X G True,1> & !<X F False,1>
loop: False | (True & (<X G True,0> <-> <X G True,1>) & (<X F False,0> <-> <X F False,1>) & True & (<X F False,1> -> (False | False)))
empty or loop: (True & !<X G True,1> & !<X F False,1>) | False | (True & (<X G True,0> <-> <X G True,1>) & (<X F False,0> <-> <X F False,1>) & True & (<X F False,1> -> (False | False)))
The formula is SAT!


> GLUCOSE:
k: 0s
k-unraveling: (False | (True & <X G True,0>)) & (False | <X F False,0> | True)
empty: True & !<X F False,0> & !<X G True,0>
loop: False
empty or loop: (True & !<X F False,0> & !<X G True,0>) | False
prune: False

k: 1
k-unraveling: True & (<X G True,0> <-> (True & <X G True,1>)) & (<X F False,0> <-> (False | <X F False,1>))
empty: True & !<X G True,1> & !<X F False,1>
loop: False | (True & (<X G True,0> <-> <X G True,1>) & (<X F False,0> <-> <X F False,1>) & True & (<X F False,1> -> (False | False)))
empty or loop: (True & !<X G True,1> & !<X F False,1>) | False | (True & (<X G True,0> <-> <X G True,1>) & (<X F False,0> <-> <X F False,1>) & True & (<X F False,1> -> (False | False)))
prune: False

k: 2
k-unraveling: True & (<X G True,1> <-> (True & <X G True,2>)) & (<X F False,1> <-> (False | <X F False,2>))
empty: True & !<X G True,2> & !<X F False,2>
loop: False | (True & (<X G True,0> <-> <X G True,2>) & (<X F False,0> <-> <X F False,2>) & True & (<X F False,2> -> (False | False | False))) | (True & (<X G True,1> <-> <X G True,2>) & (<X F False,1> <-> <X F False,2>) & True & (<X F False,2> -> (False | False)))
empty or loop: (True & !<X G True,2> & !<X F False,2>) | False | (True & (<X G True,0> <-> <X G True,2>) & (<X F False,0> <-> <X F False,2>) & True & (<X F False,2> -> (False | False | False))) | (True & (<X G True,1> <-> <X G True,2>) & (<X F False,1> <-> <X F False,2>) & True & (<X F False,2> -> (False | False)))
prune: False | False | (True & (<X G True,0> <-> <X G True,1>) & (<X F False,0> <-> <X F False,1>) & True & (<X G True,1> <-> <X G True,2>) & (<X F False,1> <-> <X F False,2>) & True & ((<X F False,2> & (False | False)) -> (False | False)))

The formula is UNSAT!