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)