1 ((((headed jar) and (forall x ((bug x) => (animal x)))) and (forall x, x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x)))) and (forall y ((forall x (((in x y) and (bug x)) => (dead x))) => (sterile y)))) Thus (sterile jar)

 1 (((headed jar) and (forall x ((bug x) => (animal x)))) and (forall x, x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x)))) 2 (forall y ((forall x (((in x y) and (bug x)) => (dead x))) => (sterile y))) Thus (sterile jar)

 1 (headed jar) 2 (forall x ((bug x) => (animal x))) 3 (forall x, x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x))) 4 (forall y ((forall x (((in x y) and (bug x)) => (dead x))) => (sterile y))) Thus (sterile jar)

 1 ((forall x (((in x jar) and (bug x)) => (dead x))) => (sterile jar)) 2 (headed jar) 3 (forall x ((bug x) => (animal x))) 4 (forall x, x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x))) 5 (forall y ((forall x (((in x y) and (bug x)) => (dead x))) => (sterile y))) Thus (sterile jar)

 Vars x 1 ((forall x1 (((in x1 jar) and (bug x1)) => (dead x1))) => (sterile jar)) 2 (headed jar) 3 (forall x1 ((bug x1) => (animal x1))) 4 (forall x1, x2 ((((headed x2) and (in x1 x2)) and (animal x1)) => (dead x1))) 5 (forall y ((forall x1 (((in x1 y) and (bug x1)) => (dead x1))) => (sterile y))) Thus (((in x jar) and (bug x)) => (dead x))

 Vars x 1 (in x jar) 2 (bug x) 3 ((forall x1 (((in x1 jar) and (bug x1)) => (dead x1))) => (sterile jar)) 4 (headed jar) 5 (forall x1 ((bug x1) => (animal x1))) 6 (forall x1, x2 ((((headed x2) and (in x1 x2)) and (animal x1)) => (dead x1))) 7 (forall y ((forall x1 (((in x1 y) and (bug x1)) => (dead x1))) => (sterile y))) Thus (dead x)

 Vars x 1 (forall x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x))) 2 (in x jar) 3 (bug x) 4 ((forall x1 (((in x1 jar) and (bug x1)) => (dead x1))) => (sterile jar)) 5 (headed jar) 6 (forall x1 ((bug x1) => (animal x1))) 7 (forall x1, x2 ((((headed x2) and (in x1 x2)) and (animal x1)) => (dead x1))) 8 (forall y ((forall x1 (((in x1 y) and (bug x1)) => (dead x1))) => (sterile y))) Thus (dead x)

 Vars x 1 ((((headed jar) and (in x jar)) and (animal x)) => (dead x)) 2 (forall x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x))) 3 (in x jar) 4 (bug x) 5 ((forall x1 (((in x1 jar) and (bug x1)) => (dead x1))) => (sterile jar)) 6 (headed jar) 7 (forall x1 ((bug x1) => (animal x1))) 8 (forall x1, x2 ((((headed x2) and (in x1 x2)) and (animal x1)) => (dead x1))) 9 (forall y ((forall x1 (((in x1 y) and (bug x1)) => (dead x1))) => (sterile y))) Thus (dead x)

 Vars x 1 ((((headed jar) and (in x jar)) and (animal x)) => (dead x)) 2 (forall x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x))) 3 (in x jar) 4 (bug x) 5 ((forall x1 (((in x1 jar) and (bug x1)) => (dead x1))) => (sterile jar)) 6 (headed jar) 7 (forall x1 ((bug x1) => (animal x1))) 8 (forall x1, x2 ((((headed x2) and (in x1 x2)) and (animal x1)) => (dead x1))) 9 (forall y ((forall x1 (((in x1 y) and (bug x1)) => (dead x1))) => (sterile y))) Thus (((headed jar) and (in x jar)) and (animal x))

 Vars x 1 ((((headed jar) and (in x jar)) and (animal x)) => (dead x)) 2 (forall x1 ((((headed x1) and (in x x1)) and (animal x)) => (dead x))) 3 (in x jar) 4 (bug x) 5 ((forall x1 (((in x1 jar) and (bug x1)) => (dead x1))) => (sterile jar)) 6 (headed jar) 7 (forall x1 ((bug x1) => (animal x1))) 8 (forall x1, x2 ((((headed x2) and (in x1 x2)) and (animal x1)) => (dead x1))) 9 (forall y ((forall x1 (((in x1 y) and (bug x1)) => (dead x1))) => (sterile y))) Thus (headed jar)