examples/wos/rigorous.in

42 % -P(x,i(i(i(i(q,r),i(p,r)),s),i(i(p,q),s))) | $ANS(neg_th_04).
43 % -P(x,i(i(p,i(q,r)),i(i(s,q),i(p,i(s,r))))) | $ANS(neg_th_05).
44 % -P(x,i(i(p,q),i(i(i(p,r),s),i(i(q,r),s)))) | $ANS(neg_th_06).
45 % -P(x,i(i(t,i(i(p,r),s)),i(i(p,q),i(t,i(i(q,r),s))))) | $ANS(neg_th_07).
46 % -P(x,i(i(q,r),i(i(p,q),i(i(r,s),i(p,s))))) | $ANS(neg_th_08).
47 % -P(x,i(i(i(n(p),q),r),i(p,r))) | $ANS(neg_th_09).
48 % -P(x,i(p,i(i(i(n(p),p),p),i(i(q,p),p)))) | $ANS(neg_th_10).
49 % -P(x,i(i(q,i(i(n(p),p),p)),i(i(n(p),p),p))) | $ANS(neg_th_11).
50 % -P(x,i(t,i(i(n(p),p),p))) | $ANS(neg_th_12).
51 % -P(x,i(i(n(p),q),i(t,i(i(q,p),p)))) | $ANS(neg_th_13).
52 % -P(x,i(i(i(t,i(i(q,p),p)),r),i(i(n(p),q),r))) | $ANS(neg_th_14).
53 % -P(x,i(i(n(p),q),i(i(q,p),p))) | $ANS(neg_th_15).
54 % -P(x,i(p,p)) | $ANS(neg_th_16).
55 % -P(x,i(p,i(i(q,p),p))) | $ANS(neg_th_17).
56 % -P(x,i(q,i(p,q))) | $ANS(neg_th_18).
57 % -P(x,i(i(i(p,q),r),i(q,r))) | $ANS(neg_th_19).
58 % -P(x,i(p,i(i(p,q),q))) | $ANS(neg_th_20).
59 % -P(x,i(i(p,i(q,r)),i(q,i(p,r)))) | $ANS(neg_th_21).
60 % -P(x,i(i(q,r),i(i(p,q),i(p,r)))) | $ANS(neg_th_22).
61 % -P(x,i(i(i(q,i(p,r)),s),i(i(p,i(q,r)),s))) | $ANS(neg_th_23).
62 % -P(x,i(i(i(p,q),p),p)) | $ANS(neg_th_24).
63 % -P(x,i(i(i(p,r),s),i(i(p,q),i(i(q,r),s)))) | $ANS(neg_th_25).
64 % -P(x,i(i(i(p,q),r),i(i(r,p),p))) | $ANS(neg_th_26).
65 % -P(x,i(i(i(p,q),q),i(i(q,p),p))) | $ANS(neg_th_27).
66 % -P(x,i(i(i(i(r,p),p),s),i(i(i(p,q),r),s))) | $ANS(neg_th_28).
67 % -P(x,i(i(i(p,q),r),i(i(p,r),r))) | $ANS(neg_th_29).
68 % -P(x,i(i(p,i(p,q)),i(p,q))) | $ANS(neg_th_30).
69 % -P(x,i(i(p,s),i(i(i(p,q),r),i(i(s,r),r)))) | $ANS(neg_th_31).
70 % -P(x,i(i(i(p,q),r),i(i(p,s),i(i(s,r),r)))) | $ANS(neg_th_32).
71 % -P(x,i(i(p,s),i(i(s,i(q,i(p,r))),i(q,i(p,r))))) | $ANS(neg_th_33).
72 % -P(x,i(i(s,i(q,i(p,r))),i(i(p,s),i(q,i(p,r))))) | $ANS(neg_th_34).
73 % -P(x,i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | $ANS(neg_th_35).
74 % -P(x,i(n(p),i(p,q))) | $ANS(neg_th_36).
75 % -P(x,i(i(i(p,q),r),i(n(p),r))) | $ANS(neg_th_37).
76 % -P(x,i(i(p,n(p)),n(p))) | $ANS(neg_th_38).
77 % -P(x,i(n(n(p)),p)) | $ANS(neg_th_39).
78 % -P(x,i(p,n(n(p)))) | $ANS(neg_th_40).
79 % -P(x,i(i(p,q),i(n(n(p)),q))) | $ANS(neg_th_41).
80 % -P(x,i(i(i(n(n(p)),q),r),i(i(p,q),r))) | $ANS(neg_th_42).
81 % -P(x,i(i(p,q),i(i(q,n(p)),n(p)))) | $ANS(neg_th_43).
82 % -P(x,i(i(s,i(q,n(p))),i(i(p,q),i(s,n(p))))) | $ANS(neg_th_44).
83 % -P(x,i(i(s,i(q,p)),i(i(n(p),q),i(s,p)))) | $ANS(neg_th_45).
84 % -P(x,i(i(p,q),i(n(q),n(p)))) | $ANS(neg_th_46).
85 % -P(x,i(i(p,n(q)),i(q,n(p)))) | $ANS(neg_th_47).
86 % -P(x,i(i(n(p),q),i(n(q),p))) | $ANS(neg_th_48).
87 % -P(x,i(i(n(p),n(q)),i(q,p))) | $ANS(neg_th_49).
88 % -P(x,i(i(i(n(q),p),r),i(i(n(p),q),r))) | $ANS(neg_th_50).
89 % -P(x,i(i(p,i(q,r)),i(p,i(n(r),n(q))))) | $ANS(neg_th_51).
90 % -P(x,i(i(p,i(q,n(r))),i(p,i(r,n(q))))) | $ANS(neg_th_52).
91 % -P(x,i(i(n(p),q),i(i(p,q),q))) | $ANS(neg_th_53).
92 % -P(x,i(i(p,q),i(i(n(p),q),q))) | $ANS(neg_th_54).
93 % -P(x,i(i(p,q),i(i(p,n(q)),n(p)))) | $ANS(neg_th_55).
94 % -P(x,i(i(i(i(p,q),q),r),i(i(n(p),q),r))) | $ANS(neg_th_56).
95 % -P(x,i(i(n(p),r),i(i(p,q),i(i(q,r),r)))) | $ANS(neg_th_57).
96 % -P(x,i(i(i(i(p,q),i(i(q,r),r)),s),i(i(n(p),r),s))) | $ANS(neg_th_58).
97 % -P(x,i(i(n(p),r),i(i(q,r),i(i(p,q),r)))) | $ANS(neg_th_59).
98 % -P(x,i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r))))) | $ANS(neg_th_60).
99 % -P(x,i(i(p,r),i(i(q,r),i(i(n(p),q),r)))) | $ANS(neg_th_61).
100 % -P(x,i(i(n(n(p)),q),i(p,q))) | $ANS(neg_th_62).
101 % -P(x,i(q,i(p,p))) | $ANS(neg_th_63).
102 % -P(x,i(n(i(p,p)),q)) | $ANS(neg_th_64).
103 % -P(x,i(i(n(q),n(i(p,p))),q)) | $ANS(neg_th_65).
104 % -P(x,i(n(i(p,q)),p)) | $ANS(neg_th_66).
105 % -P(x,i(n(i(p,q)),n(q))) | $ANS(neg_th_67).
106 % -P(x,i(n(i(p,n(q))),q)) | $ANS(neg_th_68).
107 % -P(x,i(p,i(n(q),n(i(p,q))))) | $ANS(neg_th_69).
108 % -P(x,i(p,i(q,n(i(p,n(q)))))) | $ANS(neg_th_70).
109 % -P(x,n(i(i(p,p),n(i(q,q))))) | $ANS(neg_th_71).