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) |