[traths@jk-005 Gint]$ less formula1.in 
((frm
(-> (& (all x (p x)) (exist y (q y))) (exist z (v (p z) (- (q z)))))
))
[traths@jk-005 Gint]$ ./gint formula1.in 
Starting to read file formula1.in
File read OK.(((-p x_2) (p x_2)))
input int formula: 
(-> (& (all x_2 (p x_2)) (exist y_3 (q y_3))) (exist z_1 (v (p z_1) (- (q z_1)))))
labelled int formula: 
((L1 0) : (-> ((L5 0) : (& ((L6 0) : (all x_2 (p x_2))) ((L7 0) : (exist y_3 (q y_3))))) ((L2 0) 
: (exist z_1 ((L3 z_1) : (v (p z_1) ((L4 z_1) : (- (q z_1)))))))))
********* EMPTY CLAUSE DERIVED *********


by binary from 6(3) and 9 we get:
0: 
input: 
6: (rule: +-> L1) -L2(0) | L1(0) | L5(0).
by binary from 3(2) and 8(2) we get:
9: -L5(0) | L2(0).
input: 
3: (rule: -& L5) -L5(0) | p(x).
by binary from 2(2) and 7(2) we get:
8: 
input: 
2: (rule: +exist L2) L2(0) | -p(x).
input: 
7: 

; program args: ("./gint" "formula1.in")
[traths@jk-005 Gint]$ less formula2.in 
((frm
(-> (& (exist x (p x)) (exist y (q y))) (all z (v (- (p z)) (q z))))
))
[traths@jk-005 Gint]$ ./gint formula2.in 
Starting to read file formula2.in
File read OK.(((-q cc_1z) (q cc_1z)))
input int formula: 
(-> (& (exist x_1 (p x_1)) (exist y_2 (q y_2))) (all cc_1z (v (- (p cc_1z)) (q cc_1z))))
labelled int formula: 
; program args: ("./gint" "formula2.in")
((L1 0) : (-> ((L5 0) : (& ((L6 0) : (exist x_1 (p x_1))) ((L7 0) : (exist y_2 (q y_2))))) ((L2 0) : (all cc_1z ((L3 0) : (v ((L4 0) : (- (p cc_1z))) (q cc_1z)))))))[traths@jk-005 Gint]$ 
[traths@jk-005 Gint]$ less formula3.in
((frm
(-> (v (p a) (& (- (q a)) (r a))) (& (v (p a) (- (q a))) (v (p a) (r a))))
))
[traths@jk-005 Gint]$ ./gint formula3.in
Starting to read file formula3.in
File read OK.(((-r a) (r a)) ((-q a) (q a)) ((-L8 0) (L4 0)) ((-p a) (p a)) ((-p a) (p a)))
input int formula: 
(-> (v (p a) (& (- (q a)) (r a))) (& (v (p a) (- (q a))) (v (p a) (r a))))
labelled int formula: 
((L1 0) : (-> ((L6 0) : (v (p a) ((L7 0) : (& ((L8 0) : (- (q a))) (r a))))) ((L2 0) : (& ((L3 0) : (v (p a) ((L4 0) : (- (q a))))) ((L5 0) : (v (p a) (r a)))))))
********* EMPTY CLAUSE DERIVED *********


by binary from 8(2) and 39 we get:
0: 
input: 
8: (rule: +-> L1) -L2(0) | L6(0) | L1(0).
by hyper from 10 with 34(2) 25(2)  we get:
39: -L6(0) | L2(0).
input: 
10: (rule: +& L2) -L5(0) | -L3(0) | L2(0).
by hyper from 9 with 20 17  we get:
34: -L6(0) | L5(0).
input: 
9: (rule: -v L6) -L6(0) | L7(0) | p(a).
by binary from 6(2) and 19 we get:
20: -L7(0) | L5(0).
input: 
6: (rule: -& L7) -L7(0) | r(a).
by binary from 3 and 11(2) we get:
19: 
input: 
3: (rule: +v L5) -r(a) | L5(0).
input: 
11: 
by binary from 4 and 14(2) we get:
17: -p(a) | L5(0).
input: 
4: (rule: +v L5) -p(a) | L5(0).
input: 
14: 
by hyper from 9 with 13 16  we get:
25: -L6(0) | L3(0).
input: 
13: -L7(0) | L3(0).
by binary from 2 and 14(2) we get:
16: -p(a) | L3(0).
input: 
2: (rule: +v L3) -p(a) | L3(0).
input: 
14: 

; program args: ("./gint" "formula3.in")
[traths@jk-005 Gint]$ less formula4.in
((frm
(<-> (-> ((p a) (q a))) (& (v (q a) (- (p a))) (v (- (q a)) (p a))))
))
[traths@jk-005 Gint]$ ./gint formula4.in
Starting to read file formula4.in
File read OK.()
input int formula: 
(<-> (-> ((p a) (q a))) (& (v (q a) (- (p_new2 a))) (v (- (q_new1 a)) (p_new2 a))))
labelled int formula: 
; program args: ("./gint" "formula4.in")
(<-> (-> ((p a) (q a))) (& (v (q a) (- (p_new2 a))) (v (- (q_new1 a)) (p_new2 a))))[traths@jk-005 Gint]$ 
[traths@jk-005 Gint]$