1:(input (#1:(and #2:(= b a) #3:(= b c) #4:(= c d) #5:(= e c) #6:(= e f) (not #7:(= a f)))))
2:(and (#2) 1 0)
3:(and (#3) 1 1)
4:(and (#5) 1 3)
5:(and (#6) 1 4)
6:(and ((not #7)) 1 5)
7:(eq_transitive ((not #2) (not #3) (not #5) (not #6) #7))
8:(resolution () 7 2 3 4 5 6)