lapply (H4 i); clear H4;
rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
rewrite > distributive_orb_andb;
- autobatch paramodulation by distributive_orb_andb,symm_orb,symm_orb, Hletin, Hletin1,andb_true.
+ demodulate.
+ reflexivity.
+ (*
+ autobatch paramodulation
+ by distributive_orb_andb,symm_orb,symm_orb,
+ Hletin, Hletin1,andb_true.
+ *)
| simplify in H2 ⊢ %;
intros;
lapply (H2 i); clear H2;
- autobatch paramodulation by andb_assoc, Hletin.
+ pump 100. pump 100.
+ demodulate.
+ reflexivity.
+ (* autobatch paramodulation by andb_assoc, Hletin. *)
| simplify in H2 H4 ⊢ %;
intros;
lapply (H2 i); clear H2;
rewrite > demorgan2;
rewrite > symm_orb;
rewrite > distributive_orb_andb;
- autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1.
+ demodulate.
+ reflexivity.
+ (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *)
| simplify in H2 ⊢ %;
intros;
lapply (H2 i); clear H2;