use(subst).
%use(int_lemmas).  % redundant
use(lemmaF2).

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

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

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



base,step1,step2		-> [].

/*  
some variable overlaps might be needed to derive false from
these facts:
j<k.
k<i.
p(i)=j.
*/

top_predicates_precedence([base,step1,step2,lemmaF2]).

option([var_overlaps(off),search_depth(-1),full_cnf(yes)]).
:-sarp(+[15]).
%:-sama([]).
:-saci([2]).

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