[traths@jk-005 PITP]$ less formula1 p | (~ q & r) -> (p | ~ q) & (p | r) [traths@jk-005 pitp]$ ./pitp -f formula1 Start wffs size = 10 file name = formula1 search result = provable search time = 0e-3 main loop = 12 backtracking split = 2 backtracking not safe = 0 group safe not split = 4 group safe split = 4 group F = 2 group T = 0 group split Fc = 0 group not split Fc = 0 Group F substitution = 0 Group T substitution = 0 Set Validity = 0 [traths@jk-005 pitp]$ less formula2 (p -> q) -> (q | ~ p) & (~ q | p) [traths@jk-005 pitp]$ ./pitp -f formula2 Start wffs size = 9 file name = formula2 search result = unprovable search time = 0e-3 main loop = 6 backtracking split = 0 backtracking not safe = 0 group safe not split = 2 group safe split = 1 group F = 2 group T = 0 group split Fc = 0 group not split Fc = 0 Group F substitution = 0 Group T substitution = 0 Set Validity = 1 [traths@jk-005 PITP]$