use(subst).
use(int_lemmas).
use(lemmaF2).

% Proof by induction over S
% base case
lemmaF2(var(j),k,i),

% step case for abstractions
(all(K,all(I,lemmaF2(s,K,I))) => lemmaF2(abs(s),k,i)),

% step case for applications
(lemmaF2(s,k,i) and lemmaF2(t,k,i) => lemmaF2(app(s,t),k,i)) -> [].

option([var_overlaps(off),search_depth(0)]).
:-sarp(+[15]).

/*
Proof:
======

   1 : A<A ->                                                           [input]
   3 : A<s(A)                                                           [input]
   5 : p(s(A))=A                                                        [input]
   6 : s(p(A))=A                                                        [input]
   8 : s(A)=s(B) -> A=B                                                 [input]
  13 : A=<B,s(B)=<A                                                     [input]
  20 : A<B -> lift(var(A),B)=var(A)                                     [input]
  21 : A=<B -> lift(var(B),A)=var(s(B))                                 [input]
  22 : lift(app(A,B),C)=app(lift(A,C),lift(B,C))                        [input]
  23 : lift(abs(A),B)=abs(lift(A,s(B)))                                 [input]
  24 : free(var(A),B)==(A=B)                                            [input]
  25 : free(app(A,B),C)==(free(A,C)or free(B,C))                        [input]
  26 : free(abs(A),B)==free(A,s(B))                                     [input]
  28 : A=<B -> s(A)=<s(B)                                               [input]
  30 : lemmaF2(A,B,C)==(0=<B and 0=<C=>free(lift(A,B),C)<=>free(A,p(C))and B<C or free(A,C)and C<B) [input]
  31 : lemmaF2(var(j),k,i),!A,B.(lemmaF2(s,A,B))=>lemmaF2(abs(s),k,i),lemmaF2(s,k,i)and lemmaF2(t,k,i)=>lemmaF2(app(s,t),k,i) ->  [input]
  34 : A=<B,lift(var(B),A)=var(B)                 [totality resolution from 20]
  35 : A<B,lift(var(A),B)=var(s(A))               [totality resolution from 21]
  37 : A<B,s(B)=<s(A)                             [totality resolution from 28]
  39 : !A,B.(0=<A and 0=<B=>free(lift(s,A),B)<=>free(s,p(B))and A<B or free(s,B)and B<A)=>0=<k and 0=<i=>free(lift(s,s(k)),s(i))<=>free(s,i)and k<i or free(s,s(i))and i<k,0=<k and 0=<i=>free(lift(var(j),k),i)<=>j=p(i)and k<i or j=i and i<k,(0=<k and 0=<i=>free(lift(s,k),i)<=>free(s,p(i))and k<i or free(s,i)and i<k)and(0=<k and 0=<i=>free(lift(t,k),i)<=>free(t,p(i))and k<i or free(t,i)and i<k)=>0=<k and 0=<i=>free(lift(s,k),i)or free(lift(t,k),i)<=>(free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k ->  [reduction of 31 by [30,24,24,30,26,26,6,23,26,30,30,25,25,22,25,30,30]]
  40 : p$199,!A,B.(0=<A and 0=<B=>free(lift(s,A),B)<=>free(s,p(B))and A<B or free(s,B)and B<A)=>0=<k and 0=<i=>free(lift(s,s(k)),s(i))<=>free(s,i)and k<i or free(s,s(i))and i<k,0=<k and 0=<i=>free(lift(var(j),k),i)<=>j=p(i)and k<i or j=i and i<k ->  [expansion from 39]
  41 : p$199,(0=<k and 0=<i=>free(lift(s,k),i)<=>free(s,p(i))and k<i or free(s,i)and i<k)and(0=<k and 0=<i=>free(lift(t,k),i)<=>free(t,p(i))and k<i or free(t,i)and i<k) [expansion from 39]
  42 : 0=<k and 0=<i=>free(lift(s,k),i)or free(lift(t,k),i)<=>(free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k -> p$199 [expansion from 39]
  43 : p$198,0=<k and 0=<i=>free(lift(var(j),k),i)<=>j=p(i)and k<i or j=i and i<k,p$199 ->  [expansion from 40]
  44 : p$198,!A,B.(0=<A and 0=<B=>free(lift(s,A),B)<=>free(s,p(B))and A<B or free(s,B)and B<A) [expansion from 40]
  45 : 0=<k and 0=<i=>free(lift(s,s(k)),s(i))<=>free(s,i)and k<i or free(s,s(i))and i<k -> p$198 [expansion from 40]
  46 : 0=<A,0=<B -> p$198,free(lift(s,A),B)==(free(s,p(B))and A<B or free(s,B)and B<A) [expansion from 44]
  48 : A<0,B<0,p$198,free(lift(s,B),A)==(free(s,p(A))and B<A or free(s,A)and A<B) [totality resolution from 46]
  49 : p$197,p$199                                          [expansion from 41]
  50 : p$197 -> 0=<k and 0=<i=>free(lift(s,k),i)<=>free(s,p(i))and k<i or free(s,i)and i<k [expansion from 41]
  51 : p$197 -> 0=<k and 0=<i=>free(lift(t,k),i)<=>free(t,p(i))and k<i or free(t,i)and i<k [expansion from 41]
  52 : p$197,0=<k,0=<i -> free(lift(s,k),i)==(free(s,p(i))and k<i or free(s,i)and i<k) [expansion from 50]
  54 : p$197 -> i<0,k<0,free(lift(s,k),i)==(free(s,p(i))and k<i or free(s,i)and i<k) [totality resolution from 52]
  55 : p$197,0=<k,0=<i -> free(lift(t,k),i)==(free(t,p(i))and k<i or free(t,i)and i<k) [expansion from 51]
  57 : p$197 -> i<0,k<0,free(lift(t,k),i)==(free(t,p(i))and k<i or free(t,i)and i<k) [totality resolution from 55]
  58 : p$196 -> p$199                                       [expansion from 42]
  59 : p$196,0=<k and 0=<i                                  [expansion from 42]
  60 : (free(lift(s,k),i)or free(lift(t,k),i))==((free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k) -> p$196 [expansion from 42]
  61 : free(lift(s,k),i)or free(lift(t,k),i)=>(free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k,(free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k=>free(lift(s,k),i)or free(lift(t,k),i) -> p$196 [expansion from 60]
  62 : p$195 -> p$198                                       [expansion from 45]
  63 : p$195,0=<k and 0=<i                                  [expansion from 45]
  64 : free(lift(s,s(k)),s(i))==(free(s,i)and k<i or free(s,s(i))and i<k) -> p$195 [expansion from 45]
  65 : free(lift(s,s(k)),s(i))=>free(s,i)and k<i or free(s,s(i))and i<k,free(s,i)and k<i or free(s,s(i))and i<k=>free(lift(s,s(k)),s(i)) -> p$195 [expansion from 64]
  66 : p$194,p$196                                          [expansion from 59]
  67 : p$194 -> 0=<k                                        [expansion from 59]
  68 : p$194 -> 0=<i                                        [expansion from 59]
  69 : p$193,(free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k=>free(lift(s,k),i)or free(lift(t,k),i) -> p$196 [expansion from 61]
  70 : p$193,free(lift(s,k),i)or free(lift(t,k),i)          [expansion from 61]
  71 : (free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k -> p$193 [expansion from 61]
  72 : p$193,free(lift(s,k),i),free(lift(t,k),i)            [expansion from 70]
  73 : p$194,p$195                                          [expansion from 63]
  74 : p$192,free(s,i)and k<i or free(s,s(i))and i<k=>free(lift(s,s(k)),s(i)) -> p$195 [expansion from 65]
  75 : p$192,free(lift(s,s(k)),s(i))                        [expansion from 65]
  76 : free(s,i)and k<i or free(s,s(i))and i<k -> p$192     [expansion from 65]
  77 : p$191,p$193 -> p$196                                 [expansion from 69]
  78 : p$191,(free(s,p(i))or free(t,p(i)))and k<i or(free(s,i)or free(t,i))and i<k [expansion from 69]
  79 : free(lift(s,k),i)or free(lift(t,k),i) -> p$191       [expansion from 69]
  80 : p$191,(free(s,p(i))or free(t,p(i)))and k<i,(free(s,i)or free(t,i))and i<k [expansion from 78]
  81 : p$190 -> p$193                                       [expansion from 71]
  82 : (free(s,p(i))or free(t,p(i)))and k<i -> p$190        [expansion from 71]
  83 : (free(s,i)or free(t,i))and i<k -> p$190              [expansion from 71]
  84 : free(s,p(i))or free(t,p(i)),k<i -> p$190             [expansion from 82]
  85 : free(s,p(i))or free(t,p(i)) -> i=<k,p$190  [totality resolution from 84]
  86 : free(s,i)or free(t,i),i<k -> p$190                   [expansion from 83]
  87 : free(s,i)or free(t,i) -> k=<i,p$190        [totality resolution from 86]
  88 : p$189,p$192 -> p$195                                 [expansion from 74]
  89 : p$189,free(s,i)and k<i or free(s,s(i))and i<k        [expansion from 74]
  90 : free(lift(s,s(k)),s(i)) -> p$189                     [expansion from 74]
  91 : p$189,free(s,i)and k<i,free(s,s(i))and i<k           [expansion from 89]
  92 : p$188 -> p$192                                       [expansion from 76]
  93 : free(s,i)and k<i -> p$188                            [expansion from 76]
  94 : free(s,s(i))and i<k -> p$188                         [expansion from 76]
  95 : free(s,i),k<i -> p$188                               [expansion from 93]
  96 : free(s,i) -> i=<k,p$188                    [totality resolution from 95]
  97 : free(s,s(i)),i<k -> p$188                            [expansion from 94]
  98 : free(s,s(i)) -> k=<i,p$188                 [totality resolution from 97]
  99 : p$187,p$191,(free(s,i)or free(t,i))and i<k           [expansion from 80]
 100 : p$187 -> free(s,p(i))or free(t,p(i))                 [expansion from 80]
 101 : p$187 -> k<i                                         [expansion from 80]
 102 : p$187 -> free(s,p(i)),free(t,p(i))                  [expansion from 100]
 103 : p$186 -> p$191                                       [expansion from 79]
 104 : free(lift(s,k),i) -> p$186                           [expansion from 79]
 105 : free(lift(t,k),i) -> p$186                           [expansion from 79]
 106 : p$185 -> i=<k,p$190                                  [expansion from 85]
 107 : free(s,p(i)) -> p$185                                [expansion from 85]
 108 : free(t,p(i)) -> p$185                                [expansion from 85]
 109 : p$184 -> k=<i,p$190                                  [expansion from 87]
 110 : free(s,i) -> p$184                                   [expansion from 87]
 111 : free(t,i) -> p$184                                   [expansion from 87]
 112 : p$183,p$189,free(s,i)and k<i                         [expansion from 91]
 113 : p$183 -> free(s,s(i))                                [expansion from 91]
 114 : p$183 -> i<k                                         [expansion from 91]
 115 : p$182,p$191,p$187                                    [expansion from 99]
 116 : p$182 -> free(s,i)or free(t,i)                       [expansion from 99]
 117 : p$182 -> i<k                                         [expansion from 99]
 118 : p$182 -> free(s,i),free(t,i)                        [expansion from 116]
 119 : p$181,p$189,p$183                                   [expansion from 112]
 120 : p$181 -> free(s,i)                                  [expansion from 112]
 121 : p$181 -> k<i                                        [expansion from 112]
 122 : p$196,0=<k                             [negative chaining of 66 from 67]
 123 : p$196,0=<i                             [negative chaining of 66 from 68]
 124 : p$195,0=<k                             [negative chaining of 73 from 67]
 125 : p$195,0=<i                             [negative chaining of 73 from 68]
 126 : p$191,p$187,i<k                      [negative chaining of 115 from 117]
 127 : p$189,p$183,k<i                      [negative chaining of 119 from 121]
 128 : p$189,p$183,free(s,i)                [negative chaining of 119 from 120]
 132 : p$191,p$187,free(t,i),free(s,i)      [negative chaining of 115 from 118]
 139 : p$199,free(lift(s,k),i)==(free(s,p(i))and k<i or free(s,i)and i<k),i<0,k<0 [negative chaining of 49 from 54]
 140 : p$199,free(lift(s,k),i)==(free(s,p(i))and k<i or free(s,i)and i<k) [reduction of 139 by [123,58,L,L,122,58,L,L]]
 141 : free(s,p(i))and k<i or free(s,i)and i<k -> p$199,p$186 [negative chaining of 140 from 104]
 142 : p$199,free(lift(t,k),i)==(free(t,p(i))and k<i or free(t,i)and i<k),i<0,k<0 [negative chaining of 49 from 57]
 143 : p$199,free(lift(t,k),i)==(free(t,p(i))and k<i or free(t,i)and i<k) [reduction of 142 by [123,58,L,L,122,58,L,L]]
 144 : free(t,p(i))and k<i or free(t,i)and i<k -> p$199,p$186 [negative chaining of 143 from 105]
 145 : free(t,p(i))and k<i or free(t,i)and i<k,p$193,free(lift(s,k),i),p$199 [chaining of 72 from 143]
 146 : free(t,p(i))and k<i or free(t,i)and i<k,p$193,p$199,free(s,p(i))and k<i or free(s,i)and i<k [reduction of 145 by [140]]
 147 : free(t,p(i))and k<i or free(t,i)and i<k,p$193,p$199,free(s,p(i))and k<i,free(s,i)and i<k [expansion from 146]
 148 : p$180,p$193,p$199,free(s,p(i))and k<i,free(s,i)and i<k [expansion from 147]
 149 : p$180 -> free(t,p(i))and k<i,free(t,i)and i<k       [expansion from 147]
 150 : p$179,p$193,p$199,p$180,free(s,i)and i<k            [expansion from 148]
 151 : p$179 -> free(s,p(i))                               [expansion from 148]
 152 : p$179 -> k<i                                        [expansion from 148]
 153 : p$178,p$193,p$199,p$180,p$179                       [expansion from 150]
 154 : p$178 -> free(s,i)                                  [expansion from 150]
 155 : p$178 -> i<k                                        [expansion from 150]
 156 : p$193,p$199,p$180,p$179,i<k          [negative chaining of 153 from 155]
 157 : p$193,p$199,p$180,p$179,free(s,i)    [negative chaining of 153 from 154]
 159 : p$199,p$193,p$180,p$179,p$184        [negative chaining of 157 from 110]
 161 : p$199,p$193,p$184,p$180,k<i          [negative chaining of 159 from 152]
 162 : p$199,p$193,p$184,p$180,free(s,p(i)) [negative chaining of 159 from 151]
 169 : p$199,p$193,p$184,p$180,p$185        [negative chaining of 162 from 107]
 170 : p$199,p$193,p$185,p$184,free(t,p(i))and k<i,free(t,i)and i<k [negative chaining of 169 from 149]
 171 : p$199,p$193,p$185,p$184          [reduction of 170 by [108,L,L,111,L,L]]
 172 : p$199,p$193,p$185,k=<i,p$190         [negative chaining of 171 from 109]
 173 : p$199,p$193,p$185,k=<i                      [reduction of 172 by [81,L]]
 177 : p$199,p$193,p$180,p$179,p$199,p$193,p$185     [chaining of 156 from 173]
 178 : p$180,p$179,p$199,p$193,p$185                      [condensement of 177]
 180 : p$199,p$193,p$185,p$180,free(s,p(i)) [negative chaining of 178 from 151]
 181 : p$199,p$193,p$185,p$180                    [reduction of 180 by [107,L]]
 182 : p$199,p$193,p$185,free(t,p(i))and k<i,free(t,i)and i<k [negative chaining of 181 from 149]
 183 : p$199,p$193,p$185,free(t,i)and i<k       [reduction of 182 by [108,L,L]]
 184 : p$177,p$199,p$193,p$185                             [expansion from 183]
 186 : p$177 -> i<k                                        [expansion from 183]
 187 : p$199,p$193,p$185,i<k                [negative chaining of 184 from 186]
 189 : p$199,p$193,p$185                          [reduction of 187 by [173,L]]
 190 : p$199,p$193,i=<k,p$190               [negative chaining of 189 from 106]
 191 : p$199,p$193,i=<k                            [reduction of 190 by [81,L]]
 193 : p$199,p$193,p$184,p$180,p$199,p$193           [chaining of 161 from 191]
 195 : p$184,p$180,p$199,p$193                            [condensement of 193]
 197 : p$199,p$193,p$184,free(t,p(i))and k<i,free(t,i)and i<k [negative chaining of 195 from 149]
 198 : p$199,p$193,p$184,free(t,p(i))and k<i    [reduction of 197 by [111,L,L]]
 199 : p$176,p$199,p$193,p$184                             [expansion from 198]
 201 : p$176 -> k<i                                        [expansion from 198]
 202 : p$199,p$193,p$184,k<i                [negative chaining of 199 from 201]
 204 : p$199,p$193,p$184                          [reduction of 202 by [191,L]]
 205 : p$199,p$193,k=<i,p$190               [negative chaining of 204 from 109]
 206 : k=i,p$199,p$193                         [reduction of 205 by [191,81,L]]
 218 : p$199,p$193,p$180,p$179,p$199,p$193           [chaining of 156 from 206]
 226 : p$180,p$179,p$199,p$193                            [condensement of 218]
 228 : p$199,p$193,p$180,k<i                [negative chaining of 226 from 152]
 230 : p$199,p$193,p$180                        [reduction of 228 by [206,1,L]]
 231 : p$199,p$193,free(t,p(i))and k<i,free(t,i)and i<k [negative chaining of 230 from 149]
 232 : free(t,p(i))and i<i,p$199,p$193,free(t,i)and i<i [reduction of 231 by [206,206]]
 233 : p$175,p$199,p$193,free(t,i)and i<i                  [expansion from 232]
 235 : p$175 ->                                            [expansion from 232]
 236 : free(t,i)and i<i,p$199,p$193               [reduction of 233 by [235,L]]
 237 : p$174,p$199,p$193                                   [expansion from 236]
 239 : p$174 ->                                            [expansion from 236]
 240 : p$193,p$199                                [reduction of 237 by [239,L]]
 241 : p$173 -> p$199,p$186                                [expansion from 141]
 242 : free(s,p(i))and k<i -> p$173                        [expansion from 141]
 243 : free(s,i)and i<k -> p$173                           [expansion from 141]
 244 : p$173 -> p$199               [reduction of 241 by [103,77,58,L,240,L,L]]
 245 : free(s,p(i)),k<i -> p$173                           [expansion from 242]
 246 : free(s,p(i)) -> i=<k,p$173                [totality resolution from 245]
 247 : free(s,i),i<k -> p$173                              [expansion from 243]
 248 : free(s,i) -> k=<i,p$173                   [totality resolution from 247]
 249 : p$172 -> p$199,p$186                                [expansion from 144]
 250 : free(t,p(i))and k<i -> p$172                        [expansion from 144]
 251 : free(t,i)and i<k -> p$172                           [expansion from 144]
 252 : p$172 -> p$199               [reduction of 249 by [103,77,58,L,240,L,L]]
 253 : free(t,p(i)),k<i -> p$172                           [expansion from 250]
 254 : free(t,p(i)) -> i=<k,p$172                [totality resolution from 253]
 255 : free(t,i),i<k -> p$172                              [expansion from 251]
 256 : free(t,i) -> k=<i,p$172                   [totality resolution from 255]
 260 : p$191,p$187,free(s,i),k=<i,p$172     [negative chaining of 132 from 256]
 262 : p$191,p$187,free(s,i),p$172                [reduction of 260 by [126,L]]
 284 : p$191,p$187,p$172,k=<i,p$173         [negative chaining of 262 from 248]
 285 : p$191,p$187,p$172,p$173,k=i                  [reduction of 284 by [126]]
 290 : p$191,p$187,p$191,p$187,p$173,p$172           [chaining of 126 from 285]
 302 : p$191,p$187,p$173,p$172                            [condensement of 290]
 304 : p$191,p$187,p$173,p$199              [negative chaining of 302 from 252]
 305 : p$187,p$199                  [reduction of 304 by [77,58,L,240,L,244,L]]
 306 : p$199,k<i                            [negative chaining of 305 from 101]
 307 : p$199,free(t,p(i)),free(s,p(i))      [negative chaining of 305 from 102]
 308 : p$199        [reduction of 307 by [254,252,L,306,L,L,246,244,L,306,L,L]]
 309 : 0=<k and 0=<i=>free(lift(var(j),k),i)<=>j=p(i)and k<i or j=i and i<k,p$198 ->  [reduction of 43 by [308]]
 310 : p$171,p$198 ->                                      [expansion from 309]
 312 : free(lift(var(j),k),i)==(j=p(i)and k<i or j=i and i<k) -> p$171 [expansion from 309]
 313 : free(lift(var(j),k),i)=>j=p(i)and k<i or j=i and i<k,j=p(i)and k<i or j=i and i<k=>free(lift(var(j),k),i) -> p$171 [expansion from 312]
 315 : p$170,j=p(i)and k<i or j=i and i<k=>free(lift(var(j),k),i) -> p$171 [expansion from 313]
 316 : p$170,free(lift(var(j),k),i)                        [expansion from 313]
 317 : j=p(i)and k<i or j=i and i<k -> p$170               [expansion from 313]
 318 : p$169,p$170 -> p$171                                [expansion from 315]
 319 : p$169,j=p(i)and k<i or j=i and i<k                  [expansion from 315]
 320 : free(lift(var(j),k),i) -> p$169                     [expansion from 315]
 321 : p$169,j=p(i)and k<i,j=i and i<k                     [expansion from 319]
 322 : p$168 -> p$170                                      [expansion from 317]
 323 : j=p(i)and k<i -> p$168                              [expansion from 317]
 324 : j=i and i<k -> p$168                                [expansion from 317]
 325 : j=p(i),k<i -> p$168                                 [expansion from 323]
 326 : j=p(i) -> i=<k,p$168                      [totality resolution from 325]
 327 : j=i,i<k -> p$168                                    [expansion from 324]
 328 : j=i -> k=<i,p$168                         [totality resolution from 327]
 329 : p$167,p$169,j=i and i<k                             [expansion from 321]
 330 : p$167 -> j=p(i)                                     [expansion from 321]
 331 : p$167 -> k<i                                        [expansion from 321]
 332 : p$166,p$169,p$167                                   [expansion from 329]
 333 : p$166 -> j=i                                        [expansion from 329]
 334 : p$166 -> i<k                                        [expansion from 329]
 335 : p$169,p$167,j=i                      [negative chaining of 332 from 333]
 336 : p$169,p$167,i<k                      [negative chaining of 332 from 334]
 343 : free(var(j),i),k=<j,p$170                      [chaining of 34 from 316]
 344 : free(var(s(j)),i),j<k,p$170                    [chaining of 35 from 316]
 347 : p$170,k=<j,j=i                              [reduction of 343 by [24,L]]
 348 : p$170,j<k,s(j)=i                            [reduction of 344 by [24,L]]
 355 : j<i,p$170,j<k                                   [chaining of 3 from 348]
 356 : p(i)=j,p$170,j<k                                [chaining of 348 from 5]
 359 : i=<A,A=<j,p$170,j<k {[conj([s(j)>A],[],[])]}   [chaining of 13 from 348]
 365 : i=<A,A=<j,p$170 {[conj([s(j)>A],[],[])]}   [reduction of 359 by [347,L]]
 369 : p$170,j=i,p$170,j<i                           [chaining of 347 from 355]
 373 : j=<i,p$170                                         [condensement of 369]
 386 : p$170,j<k,i=<k,p$168                 [negative chaining of 356 from 326]
 389 : i=<k,p$170                           [reduction of 386 by [365,L,322,L]]
 392 : i=<j,p$170,j=i,p$170                          [chaining of 347 from 389]
 393 : i=<j,p$170                                         [condensement of 392]
 394 : p$170,i=j                                    [reduction of 393 by [373]]
 395 : p$170,k=<i,p$168                     [negative chaining of 394 from 328]
 399 : k=i,p$170                              [reduction of 395 by [389,322,L]]
 415 : j<i,p$170,j<i,p$170                           [chaining of 355 from 399]
 421 : j<i,p$170                                          [condensement of 415]
 422 : p$170                                    [reduction of 421 by [394,1,L]]
 423 : p$169 -> p$171                               [reduction of 318 by [422]]
 428 : free(var(s(j)),i) -> j<k,p$169        [negative chaining of 35 from 320]
 430 : free(lift(var(i),k),i) -> p$169,p$167,p$169 [negative chaining of 335 from 320]
 433 : s(j)=i -> p$169,j<k                         [reduction of 428 by [24,L]]
 434 : free(lift(var(i),k),i) -> p$167,p$169              [condensement of 430]
 435 : p$169,p$167                        [reduction of 434 by [34,336,L,24,L]]
 436 : p$169,k<i                            [negative chaining of 435 from 331]
 437 : p$169,p(i)=j                         [negative chaining of 435 from 330]
 444 : s(j)=i,p$169                                    [chaining of 437 from 6]
 463 : i=<A,A=<j,p$169 {[conj([s(j)>A],[],[])]}       [chaining of 13 from 444]
 473 : p$169,p$169,j<k                      [negative chaining of 444 from 433]
 475 : p$169,j<k                                          [condensement of 473]
 476 : p$169                                [reduction of 475 by [463,436,L,L]]
 477 : p$171                                        [reduction of 423 by [476]]
 478 : p$198 ->                                     [reduction of 310 by [477]]
 479 : free(lift(s,A),B)==(free(s,p(B))and A<B or free(s,B)and B<A),A<0,B<0 [reduction of 48 by [478,L]]
 480 : p$195 ->                                    [reduction of 62 by [478,L]]
 481 : p$189,p$192 ->                              [reduction of 88 by [480,L]]
 483 : 0=<k                                       [reduction of 124 by [480,L]]
 484 : 0=<i                                       [reduction of 125 by [480,L]]
 491 : free(s,p(s(i)))and s(k)<s(i)or free(s,s(i))and s(i)<s(k) -> s(k)<0,s(i)<0,p$189 [negative chaining of 479 from 90]
 492 : free(s,p(s(i)))and s(k)<s(i)or free(s,s(i))and s(i)<s(k),p$192,s(k)<0,s(i)<0 [chaining of 75 from 479]
 494 : free(s,i)and s(k)<s(i)or free(s,s(i))and s(i)<s(k) -> p$189 [reduction of 491 by [5,3,483,L,3,484,L]]
 495 : free(s,i)and s(k)<s(i)or free(s,s(i))and s(i)<s(k),p$192 [reduction of 492 by [5,3,483,L,3,484,L]]
 496 : p$165,p$192                                         [expansion from 495]
 497 : p$165 -> free(s,i)and s(k)<s(i),free(s,s(i))and s(i)<s(k) [expansion from 495]
 498 : p$192,free(s,s(i))and s(i)<s(k),free(s,i)and s(k)<s(i) [negative chaining of 496 from 497]
 499 : p$164,p$192,free(s,i)and s(k)<s(i)                  [expansion from 498]
 500 : p$164 -> free(s,s(i))                               [expansion from 498]
 501 : p$164 -> s(i)<s(k)                                  [expansion from 498]
 502 : p$163,p$192,p$164                                   [expansion from 499]
 503 : p$163 -> free(s,i)                                  [expansion from 499]
 504 : p$163 -> s(k)<s(i)                                  [expansion from 499]
 505 : p$192,p$164,free(s,i)                [negative chaining of 502 from 503]
 506 : p$192,p$164,s(k)<s(i)                [negative chaining of 502 from 504]
 508 : p$192,p$164,i=<k,p$188                [negative chaining of 505 from 96]
 510 : p$192,p$164,i=<k                            [reduction of 508 by [92,L]]
 536 : k<s(i),p$192,p$164                              [chaining of 3 from 506]
 542 : k<A,A=<i,p$192,p$164 {[conj([s(i)>A],[],[])]}  [chaining of 13 from 536]
 546 : p$164,p$192,k=<i                         [variable elimination from 542]
 547 : p$164,p$192,k=i                              [reduction of 546 by [510]]
 562 : p$192,p$164,p$192,p$164                       [chaining of 547 from 506]
 571 : p$192,p$164                                        [condensement of 562]
 572 : p$192,s(i)<s(k)                      [negative chaining of 571 from 501]
 573 : p$192,free(s,s(i))                   [negative chaining of 571 from 500]
 574 : s(i)<A,A=<k,p$192 {[conj([s(k)>A],[],[])]}     [chaining of 13 from 572]
 580 : p$192,s(i)=<k                            [variable elimination from 574]
 583 : i<k,p$192                                       [chaining of 3 from 580]
 596 : p$162 -> p$189                                      [expansion from 494]
 597 : free(s,i)and s(k)<s(i) -> p$162                     [expansion from 494]
 598 : free(s,s(i))and s(i)<s(k) -> p$162                  [expansion from 494]
 599 : free(s,i),s(k)<s(i) -> p$162                        [expansion from 597]
 600 : free(s,i) -> s(i)=<s(k),p$162             [totality resolution from 599]
 601 : free(s,s(i)),s(i)<s(k) -> p$162                     [expansion from 598]
 602 : free(s,s(i)) -> s(k)=<s(i),p$162          [totality resolution from 601]
 608 : p$189,p$183,s(i)=<s(k),p$162         [negative chaining of 128 from 600]
 611 : i=k,p$189,p$183                 [reduction of 608 by [37,127,L,8,596,L]]
 625 : p$189,p$183,p$189,p$183                       [chaining of 127 from 611]
 638 : p$189,p$183                                        [condensement of 625]
 640 : p$189,i<k                            [negative chaining of 638 from 114]
 641 : p$189,free(s,s(i))                   [negative chaining of 638 from 113]
 642 : i<k                                    [reduction of 640 by [481,583,L]]
 643 : free(s,s(i))                           [reduction of 641 by [481,573,L]]
 646 : p$188                                   [reduction of 98 by [643,642,L]]
 655 : p$162,k=i                         [reduction of 602 by [643,37,642,L,8]]
 657 : p$192                                         [reduction of 92 by [646]]
 666 : p$189 ->                                     [reduction of 481 by [657]]
 669 : p$162 ->                                   [reduction of 596 by [666,L]]
 675 : k=i                                        [reduction of 655 by [669,L]]
 682 : false                                    [reduction of 642 by [675,1,L]]

Length = 311, Depth = 102



Total time: 329230 milliseconds

Number of forward inferences: 308
Number of tableau inferences: 114
Number of kept clauses: 366
*/