Seventy-Five Problems for Testing Automatic Theorem Provers (Was: Fuck the nazi-retards)

Hi,
It is a variant from here Problem 71 (Page 212):
71. (U-problems, after Alasdair Urquhart
U_1: (P_1 <-> P_1)
U_2: (P_1 <-> (P_2 <-> (P1 <-> P2)))
ETc..
In this paper which has full text access:
Seventy-Five Problems for Testing Automatic Theorem Provers.
Francis Jeffry Pelletier -June 1986
Journal of Automated Reasoning 2(2):191-216
DOI: 10.1007/BF02432151
https://www.researchgate.net/publication/220531947
Have Fun!
Bye
To have U_n, you need a furter variant of nastyXXX/2
Prolog code to generate it. I showed something different
but similar, with nasty1/2 and nasty2/2.
Mild Shock schrieb:

Julio Di Egidio schrieb:

*What* pelletier statements??

solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
  >>> WTF is that??  Is it INTUITIONISTIC??  Is it AFFINE??
 I compared to classical, just like your "neg" is supposed to do.