./scan_main.pl [any propositional tautology] "X"
$T
./scan_main.pl "imp(box(X),X)" "X"
(all x0 explworacc(x0,x0))
./scan_main.pl "imp(box(X),box(box(X)))" "X"
(all x0 all x1 ((all x2 (-explworacc(x1,x2) | explworacc(x0,x2))) | -explworacc(x0,x1)))
./scan_main.pl "imp(X,box(dia(X)))" "X"
(all x0 all x1 (-explworacc(x0,x1) | explworacc(x1,x0)))
./scan_main.pl "imp(dia(X),box(dia(X)))" "X"
(all x0 all x1 ((all x2 (-explworacc(x0,x2) | explworacc(x2,x1))) | -explworacc(x0,x1)))
