1:(input ((not #1:(=> #2:(= #3:(- x 3) 7) #4:(<= 10 x))))) 2:(tmp_LA_pre ((not #5:(=> #6:(and #7:(<= #3 7) #8:(<= 7 #3)) #4))) 1) 3:(not_implies1 (#6) 2) 4:(and (#8) 3 1) 5:(not_implies2 ((not #4)) 2) 6:(la_generic (#4 (not #8))) 7:(resolution () 6 4 5)