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

lemmaF2(S,K,I).

/* these should be built into the variable elimination rules
(s(X)=<s(Y))==(X=<Y).
(p(X)=<p(Y))==(X=<Y).
(s(X)<s(Y))==(X<Y).
(p(X)<p(Y))==(X<Y).
*/




goal
% Proof by induction over t
% base case
(0=<j => lemmaF3(var(j),s,k,l)),

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

% step case for applications
all(K,all(I,(lemmaF3(t,s,K,I) and lemmaF3(u,s,K,I)))) => lemmaF3(app(t,u),s,k,i) -> [].

option([var_overlaps(off),search_depth(-1),full_cnf(yes)]).
%:-sama([]),sarp(+[15]),saci([2]). % 20031216 mpino2202 122.8 s
:-sarp(+[15]),saci([2]).           % 20031216 mpino2202 70.3 s
%:-sarp(+[15]).                    % 20031216 mpino2202 76.7 s

top_predicates_precedence([lemmaF3,lemmaF2]).


/*
Proof:
======

   7 : s(A)=s(B) -> A=B                                                 [input]
   9 : p(s(A))=A                                                        [input]
  10 : s(p(A))=A                                                        [input]
  11 : A<s(A)                                                           [input]
  12 : A<B -> s(A)=<B                                                   [input]
  13 : A<B -> A=<p(B)                                                   [input]
  14 : A<B -> subst(var(B),A,C)=var(p(B))                               [input]
  15 : subst(var(A),A,B)=B                                              [input]
  16 : A<B -> subst(var(A),B,C)=var(A)                                  [input]
  17 : subst(app(A,B),C,D)=app(subst(A,C,D),subst(B,C,D))               [input]
  18 : subst(abs(A),B,C)=abs(subst(A,s(B),lift(C,0)))                   [input]
  23 : free(var(A),B)==(A=B)                                            [input]
  24 : free(app(A,B),C)==(free(A,C)or free(B,C))                        [input]
  25 : free(abs(A),B)==free(A,s(B))                                     [input]
  27 : A=<B -> s(A)=<s(B)                                               [input]
  29 : lemmaF3(A,B,C,D)==(0=<D and 0=<C=>free(subst(A,C,B),D)<=>free(A,C)and free(B,D)or(D<C and free(A,D)or C=<D and free(A,s(D)))) [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(A,B,C)                                                   [input]
  32 + 0=<j=>lemmaF3(var(j),s,k,l),!A,B,C.(lemmaF3(t,C,A,B))=>lemmaF3(abs(t),s,k,i),!D,E.(lemmaF3(t,s,D,E)and lemmaF3(u,s,D,E))=>lemmaF3(app(t,u),s,k,i) ->  [input]
  33 : A=<B,s(B)=<A                               [totality resolution from 12]
  34 : A=<B,B=<p(A)                               [totality resolution from 13]
  35 : A=<B,subst(var(A),B,C)=var(p(A))           [totality resolution from 14]
  36 : A=<B,subst(var(B),A,C)=var(B)              [totality resolution from 16]
  40 : A<B,s(B)=<s(A)                             [totality resolution from 27]
  42 : 0=<A and 0=<B=>free(lift(C,A),B)<=>free(C,p(B))and A<B or free(C,B)and B<A [reduction of 31 by [30]]
  43 : 0=<A,0=<B -> free(lift(C,A),B)==(free(C,p(B))and A<B or free(C,B)and B<A) [expansion from 42]
  45 : A<0,B<0,free(lift(C,B),A)==(free(C,p(A))and B<A or free(C,A)and A<B) [totality resolution from 43]
  46 + !A,B,C.(0=<B and 0=<A=>free(subst(t,A,C),B)<=>free(t,A)and free(C,B)or(B<A and free(t,B)or A=<B and free(t,s(B))))=>0=<i and 0=<k=>free(subst(t,s(k),lift(s,0)),s(i))<=>free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i)))),0=<j=>0=<l and 0=<k=>free(subst(var(j),k,s),l)<=>j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)),!D,E.((0=<E and 0=<D=>free(subst(t,D,s),E)<=>free(t,D)and free(s,E)or(E<D and free(t,E)or D=<E and free(t,s(E))))and(0=<E and 0=<D=>free(subst(u,D,s),E)<=>free(u,D)and free(s,E)or(E<D and free(u,E)or D=<E and free(u,s(E)))))=>0=<i and 0=<k=>free(subst(t,k,s),i)or free(subst(u,k,s),i)<=>(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i)))) ->  [reduction of 32 by [29,23,23,23,29,25,25,25,18,25,29,29,24,24,24,17,24,29,29]]
  47 + p$499,0=<j=>0=<l and 0=<k=>free(subst(var(j),k,s),l)<=>j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)),!A,B.((0=<B and 0=<A=>free(subst(t,A,s),B)<=>free(t,A)and free(s,B)or(B<A and free(t,B)or A=<B and free(t,s(B))))and(0=<B and 0=<A=>free(subst(u,A,s),B)<=>free(u,A)and free(s,B)or(B<A and free(u,B)or A=<B and free(u,s(B)))))=>0=<i and 0=<k=>free(subst(t,k,s),i)or free(subst(u,k,s),i)<=>(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i)))) ->  [expansion from 46]
  48 + p$499,!A,B,C.(0=<B and 0=<A=>free(subst(t,A,C),B)<=>free(t,A)and free(C,B)or(B<A and free(t,B)or A=<B and free(t,s(B)))) [expansion from 46]
  49 + 0=<i and 0=<k=>free(subst(t,s(k),lift(s,0)),s(i))<=>free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i)))) -> p$499 [expansion from 46]
  50 + 0=<A,0=<B -> p$499,free(subst(t,B,C),A)==(free(t,B)and free(C,A)or(A<B and free(t,A)or B=<A and free(t,s(A)))) [expansion from 48]
  52 + A<0,B<0,p$499,free(subst(t,A,C),B)==(free(t,A)and free(C,B)or(B<A and free(t,B)or A=<B and free(t,s(B)))) [totality resolution from 50]
  53 + p$498,0=<j=>0=<l and 0=<k=>free(subst(var(j),k,s),l)<=>j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)),p$499 ->  [expansion from 47]
  54 + p$498,!A,B.((0=<B and 0=<A=>free(subst(t,A,s),B)<=>free(t,A)and free(s,B)or(B<A and free(t,B)or A=<B and free(t,s(B))))and(0=<B and 0=<A=>free(subst(u,A,s),B)<=>free(u,A)and free(s,B)or(B<A and free(u,B)or A=<B and free(u,s(B))))) [expansion from 47]
  55 + 0=<i and 0=<k=>free(subst(t,k,s),i)or free(subst(u,k,s),i)<=>(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i)))) -> p$498 [expansion from 47]
  56 + p$498,(0=<A and 0=<B=>free(subst(t,B,s),A)<=>free(t,B)and free(s,A)or(A<B and free(t,A)or B=<A and free(t,s(A))))and(0=<A and 0=<B=>free(subst(u,B,s),A)<=>free(u,B)and free(s,A)or(A<B and free(u,A)or B=<A and free(u,s(A)))) [expansion from 54]
  57 + p$497 -> p$499                                       [expansion from 49]
  58 + p$497,0=<i and 0=<k                                  [expansion from 49]
  59 + free(subst(t,s(k),lift(s,0)),s(i))==(free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i))))) -> p$497 [expansion from 49]
  60 + free(subst(t,s(k),lift(s,0)),s(i))=>free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i)))),free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i))))=>free(subst(t,s(k),lift(s,0)),s(i)) -> p$497 [expansion from 59]
  61 + p$496,p$498,p$499 ->                                 [expansion from 53]
  63 + 0=<l and 0=<k=>free(subst(var(j),k,s),l)<=>j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)) -> p$496 [expansion from 53]
  64 + p$495(A,B),p$498                                     [expansion from 56]
  65 + p$495(A,B) -> 0=<B and 0=<A=>free(subst(t,A,s),B)<=>free(t,A)and free(s,B)or(B<A and free(t,B)or A=<B and free(t,s(B))) [expansion from 56]
  66 + p$495(A,B) -> 0=<B and 0=<A=>free(subst(u,A,s),B)<=>free(u,A)and free(s,B)or(B<A and free(u,B)or A=<B and free(u,s(B))) [expansion from 56]
  67 + p$495(A,B),0=<B,0=<A -> free(subst(t,A,s),B)==(free(t,A)and free(s,B)or(B<A and free(t,B)or A=<B and free(t,s(B)))) [expansion from 65]
  69 + p$495(A,B) -> A<0,B<0,free(subst(t,A,s),B)==(free(t,A)and free(s,B)or(B<A and free(t,B)or A=<B and free(t,s(B)))) [totality resolution from 67]
  70 + p$495(A,B),0=<B,0=<A -> free(subst(u,A,s),B)==(free(u,A)and free(s,B)or(B<A and free(u,B)or A=<B and free(u,s(B)))) [expansion from 66]
  72 + p$495(A,B) -> A<0,B<0,free(subst(u,A,s),B)==(free(u,A)and free(s,B)or(B<A and free(u,B)or A=<B and free(u,s(B)))) [totality resolution from 70]
  73 + p$494 -> p$498                                       [expansion from 55]
  74 + p$494,0=<i and 0=<k                                  [expansion from 55]
  75 + (free(subst(t,k,s),i)or free(subst(u,k,s),i))==((free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i))))) -> p$494 [expansion from 55]
  76 + free(subst(t,k,s),i)or free(subst(u,k,s),i)=>(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i)))),(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i))))=>free(subst(t,k,s),i)or free(subst(u,k,s),i) -> p$494 [expansion from 75]
  77 + p$493,p$497                                          [expansion from 58]
  78 + p$493 -> 0=<i                                        [expansion from 58]
  79 + p$493 -> 0=<k                                        [expansion from 58]
  80 + p$492,free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i))))=>free(subst(t,s(k),lift(s,0)),s(i)) -> p$497 [expansion from 60]
  81 + p$492,free(subst(t,s(k),lift(s,0)),s(i))             [expansion from 60]
  82 + free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i)))) -> p$492 [expansion from 60]
  83 + p$491 -> p$496                                       [expansion from 63]
  85 + free(subst(var(j),k,s),l)==(j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l))) -> p$491 [expansion from 63]
  86 + free(subst(var(j),k,s),l)=>j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)),j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l))=>free(subst(var(j),k,s),l) -> p$491 [expansion from 85]
  87 + p$493,p$494                                          [expansion from 74]
  88 + p$490,(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i))))=>free(subst(t,k,s),i)or free(subst(u,k,s),i) -> p$494 [expansion from 76]
  89 + p$490,free(subst(t,k,s),i)or free(subst(u,k,s),i)    [expansion from 76]
  90 + (free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i)))) -> p$490 [expansion from 76]
  91 + p$490,free(subst(t,k,s),i),free(subst(u,k,s),i)      [expansion from 89]
  92 + p$489,p$492 -> p$497                                 [expansion from 80]
  93 + p$489,free(t,s(k))and free(s,i)or(i<k and free(t,s(i))or k=<i and free(t,s(s(i)))) [expansion from 80]
  94 + free(subst(t,s(k),lift(s,0)),s(i)) -> p$489          [expansion from 80]
  95 + p$489,free(t,s(k))and free(s,i),i<k and free(t,s(i)),k=<i and free(t,s(s(i))) [expansion from 93]
  96 + p$488 -> p$492                                       [expansion from 82]
  97 + free(t,s(k))and free(s,i) -> p$488                   [expansion from 82]
  98 + i<k and free(t,s(i))or k=<i and free(t,s(s(i))) -> p$488 [expansion from 82]
  99 + free(t,s(k)),free(s,i) -> p$488                      [expansion from 97]
 103 + p$486,j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l))=>free(subst(var(j),k,s),l) -> p$491 [expansion from 86]
 104 + p$486,free(subst(var(j),k,s),l)                      [expansion from 86]
 105 + j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)) -> p$486 [expansion from 86]
 106 + p$485,p$490 -> p$494                                 [expansion from 88]
 107 + p$485,(free(t,k)or free(u,k))and free(s,i)or(i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i)))) [expansion from 88]
 108 + free(subst(t,k,s),i)or free(subst(u,k,s),i) -> p$485 [expansion from 88]
 109 + p$485,(free(t,k)or free(u,k))and free(s,i),i<k and(free(t,i)or free(u,i)),k=<i and(free(t,s(i))or free(u,s(i))) [expansion from 107]
 110 + p$484 -> p$490                                       [expansion from 90]
 111 + (free(t,k)or free(u,k))and free(s,i) -> p$484        [expansion from 90]
 112 + i<k and(free(t,i)or free(u,i))or k=<i and(free(t,s(i))or free(u,s(i))) -> p$484 [expansion from 90]
 113 + free(t,k)or free(u,k),free(s,i) -> p$484            [expansion from 111]
 114 + p$483,p$489,i<k and free(t,s(i)),free(t,s(k))and free(s,i) [expansion from 95]
 115 + p$483 -> k=<i                                        [expansion from 95]
 116 + p$483 -> free(t,s(s(i)))                             [expansion from 95]
 117 + p$482 -> p$488                                       [expansion from 98]
 118 + i<k and free(t,s(i)) -> p$482                        [expansion from 98]
 119 + k=<i and free(t,s(s(i))) -> p$482                    [expansion from 98]
 120 + i<k,free(t,s(i)) -> p$482                           [expansion from 118]
 121 + free(t,s(i)) -> k=<i,p$482                [totality resolution from 120]
 122 + k=<i,free(t,s(s(i))) -> p$482                       [expansion from 119]
 123 + free(t,s(s(i))) -> i<k,p$482              [totality resolution from 122]
 124 + p$481,p$486 -> p$491                                [expansion from 103]
 125 + p$481,j=k and free(s,l)or(l<k and j=l or k=<l and j=s(l)) [expansion from 103]
 126 + free(subst(var(j),k,s),l) -> p$481                  [expansion from 103]
 127 + p$481,j=k and free(s,l),l<k and j=l,k=<l and j=s(l) [expansion from 125]
 128 + p$480 -> p$486                                      [expansion from 105]
 129 + j=k and free(s,l) -> p$480                          [expansion from 105]
 130 + l<k and j=l or k=<l and j=s(l) -> p$480             [expansion from 105]
 131 + j=k,free(s,l) -> p$480                              [expansion from 129]
 132 + p$479,p$485,i<k and(free(t,i)or free(u,i)),(free(t,k)or free(u,k))and free(s,i) [expansion from 109]
 133 + p$479 -> k=<i                                       [expansion from 109]
 134 + p$479 -> free(t,s(i))or free(u,s(i))                [expansion from 109]
 135 + p$479 -> free(t,s(i)),free(u,s(i))                  [expansion from 134]
 136 + p$478 -> p$485                                      [expansion from 108]
 137 + free(subst(t,k,s),i) -> p$478                       [expansion from 108]
 138 + free(subst(u,k,s),i) -> p$478                       [expansion from 108]
 139 + p$477,free(s,i) -> p$484                            [expansion from 113]
 140 + free(t,k) -> p$477                                  [expansion from 113]
 141 + free(u,k) -> p$477                                  [expansion from 113]
 142 + p$476 -> p$484                                      [expansion from 112]
 143 + i<k and(free(t,i)or free(u,i)) -> p$476             [expansion from 112]
 144 + k=<i and(free(t,s(i))or free(u,s(i))) -> p$476      [expansion from 112]
 145 + i<k,free(t,i)or free(u,i) -> p$476                  [expansion from 143]
 146 + free(t,i)or free(u,i) -> k=<i,p$476       [totality resolution from 145]
 147 + k=<i,free(t,s(i))or free(u,s(i)) -> p$476           [expansion from 144]
 148 + free(t,s(i))or free(u,s(i)) -> i<k,p$476  [totality resolution from 147]
 149 + p$475,p$489,p$483,i<k and free(t,s(i))              [expansion from 114]
 150 + p$475 -> free(t,s(k))                               [expansion from 114]
 151 + p$475 -> free(s,i)                                  [expansion from 114]
 152 + p$474,p$481,l<k and j=l,k=<l and j=s(l)             [expansion from 127]
 153 + p$474 -> j=k                                        [expansion from 127]
 154 + p$474 -> free(s,l)                                  [expansion from 127]
 155 + p$473 -> p$480                                      [expansion from 130]
 156 + l<k and j=l -> p$473                                [expansion from 130]
 157 + k=<l and j=s(l) -> p$473                            [expansion from 130]
 158 + l<k,j=l -> p$473                                    [expansion from 156]
 159 + j=l -> k=<l,p$473                         [totality resolution from 158]
 160 + j=l -> k=<j,p$473                                  [condensement of 159]
 161 + k=<l,j=s(l) -> p$473                                [expansion from 157]
 162 + j=s(l) -> l<k,p$473                       [totality resolution from 161]
 163 + p$472,p$485,p$479,i<k and(free(t,i)or free(u,i))    [expansion from 132]
 164 + p$472 -> free(t,k)or free(u,k)                      [expansion from 132]
 165 + p$472 -> free(s,i)                                  [expansion from 132]
 166 + p$472 -> free(t,k),free(u,k)                        [expansion from 164]
 167 + p$471 -> k=<i,p$476                                 [expansion from 146]
 168 + free(t,i) -> p$471                                  [expansion from 146]
 169 + free(u,i) -> p$471                                  [expansion from 146]
 170 + p$470 -> i<k,p$476                                  [expansion from 148]
 171 + free(t,s(i)) -> p$470                               [expansion from 148]
 172 + free(u,s(i)) -> p$470                               [expansion from 148]
 173 + p$469,p$489,p$483,p$475                             [expansion from 149]
 174 + p$469 -> i<k                                        [expansion from 149]
 175 + p$469 -> free(t,s(i))                               [expansion from 149]
 176 + p$468,p$481,p$474,l<k and j=l                       [expansion from 152]
 177 + p$468 -> k=<l                                       [expansion from 152]
 178 + p$468 -> j=s(l)                                     [expansion from 152]
 179 + p$467,p$485,p$479,p$472                             [expansion from 163]
 180 + p$467 -> i<k                                        [expansion from 163]
 181 + p$467 -> free(t,i)or free(u,i)                      [expansion from 163]
 182 + p$467 -> free(t,i),free(u,i)                        [expansion from 181]
 183 + p$466,p$481,p$474,p$468                             [expansion from 176]
 184 + p$466 -> l<k                                        [expansion from 176]
 185 + p$466 -> j=l                                        [expansion from 176]
 186 + p$497,0=<i                             [negative chaining of 77 from 78]
 187 + p$497,0=<k                             [negative chaining of 77 from 79]
 188 + p$494,0=<i                             [negative chaining of 87 from 78]
 189 + p$494,0=<k                             [negative chaining of 87 from 79]
 193 + p$489,p$483,p$475,i<k                [negative chaining of 173 from 174]
 194 + p$489,p$483,p$475,free(t,s(i))       [negative chaining of 173 from 175]
 195 + p$485,p$479,p$472,i<k                [negative chaining of 179 from 180]
 196 + p$485,p$479,p$472,free(u,i),free(t,i) [negative chaining of 179 from 182]
 201 + free(var(j),l) -> k=<j,p$481          [negative chaining of 36 from 126]
 202 + free(var(j),l),k=<j,p$486                      [chaining of 36 from 104]
 203 + j=l -> p$481,k=<j                           [reduction of 201 by [23,L]]
 204 + j=l -> p$481,k=<j                                  [condensement of 203]
 205 + p$486,k=<j                [reduction of 202 by [23,L,160,155,128,L,L,L]]
 211 + free(var(p(j)),l) -> j=<k,p$481       [negative chaining of 35 from 126]
 212 + free(var(p(j)),l),j=<k,p$486                   [chaining of 35 from 104]
 213 + p(j)=l -> p$481,j=<k                        [reduction of 211 by [23,L]]
 214 + p(j)=l,p$486,j=k                        [reduction of 212 by [23,L,205]]
 215 + s(l)=j,p$486,k=j                               [chaining of 214 from 10]
 218 + A=<l,j=<A,p$486,k=j                            [chaining of 34 from 214]
 223 + p$486,k=j,l<k,p$473                  [negative chaining of 215 from 162]
 229 + p$486,k=j                  [reduction of 223 by [218,205,L,155,128,L,L]]
 235 + free(s,l) -> p$486,p$480             [negative chaining of 229 from 131]
 241 + free(subst(var(j),j,s),l),p$486,p$486         [chaining of 229 from 104]
 246 + free(s,l) -> p$486                         [reduction of 235 by [128,L]]
 247 + free(subst(var(j),j,s),l),p$486                    [condensement of 241]
 248 + p$486                                   [reduction of 247 by [15,246,L]]
 249 + p$481 -> p$491                               [reduction of 124 by [248]]
 250 + p$481,p$474,p$468,l<k                [negative chaining of 183 from 184]
 251 + p$481,p$474,p$468,l=j                [negative chaining of 183 from 185]
 258 + p$481,p$474,p$468,p$481,k=<j         [negative chaining of 251 from 204]
 259 + j<k,p$481,p$474,p$468,p$481,p$474,p$468       [chaining of 250 from 251]
 263 + p$474,p$468,p$481,k=<j                             [condensement of 258]
 264 + j<k,p$481,p$474,p$468                              [condensement of 259]
 265 + p$468,p$474,p$481                          [reduction of 264 by [263,L]]
 266 + p$474,p$481,k=<l                     [negative chaining of 265 from 177]
 267 + p$474,p$481,s(l)=j                   [negative chaining of 265 from 178]
 272 + l<j,p$481,p$474                                [chaining of 11 from 267]
 273 + p(j)=l,p$481,p$474                              [chaining of 267 from 9]
 309 + k<j,p$481,p$474,p$481,p$474                   [chaining of 266 from 272]
 312 + k<j,p$481,p$474                                    [condensement of 309]
 324 + p$481,p$474,p$481,j=<k               [negative chaining of 273 from 213]
 325 + p$474,p$481,j=<k                                   [condensement of 324]
 326 + p$474,p$481                                [reduction of 325 by [312,L]]
 327 + p$481,k=j                            [negative chaining of 326 from 153]
 328 + p$481,free(s,l)                      [negative chaining of 326 from 154]
 337 + free(subst(var(j),j,s),l) -> p$481,p$481 [negative chaining of 327 from 126]
 346 + free(subst(var(j),j,s),l) -> p$481                 [condensement of 337]
 347 + p$481                                     [reduction of 346 by [15,328]]
 349 + p$491                                        [reduction of 249 by [347]]
 351 + p$496                                         [reduction of 83 by [349]]
 352 + p$499,p$498 ->                                [reduction of 61 by [351]]
 353 + free(t,k)and free(s,i)or(i<k and free(t,i)or k=<i and free(t,s(i))),p$495(k,i) -> k<0,i<0,p$478 [negative chaining of 69 from 137]
 354 + free(u,k)and free(s,i)or(i<k and free(u,i)or k=<i and free(u,s(i))),p$495(k,i) -> k<0,i<0,p$478 [negative chaining of 72 from 138]
 355 + p$495(k,i) -> free(u,k)and free(s,i)or(i<k and free(u,i)or k=<i and free(u,s(i))),k<0,i<0,p$490,free(subst(t,k,s),i) [chaining of 72 from 91]
 356 + p$495(k,i) -> free(u,k)and free(s,i)or(i<k and free(u,i)or k=<i and free(u,s(i))),k<0,i<0,p$490,free(t,k)and free(s,i)or(i<k and free(t,i)or k=<i and free(t,s(i))) [reduction of 355 by [69]]
 357 + p$495(k,i) -> k<0,i<0,p$490,free(u,k)and free(s,i),free(t,k)and free(s,i),i<k and free(u,i),k=<i and free(u,s(i)),i<k and free(t,i),k=<i and free(t,s(i)) [expansion from 356]
 358 + p$495(k,i) -> p$465,k<0,i<0,p$490,free(t,k)and free(s,i),i<k and free(u,i),i<k and free(t,i),k=<i and free(t,s(i)),free(u,k)and free(s,i) [expansion from 357]
 359 + p$465 -> k=<i                                       [expansion from 357]
 360 + p$465 -> free(u,s(i))                               [expansion from 357]
 361 + p$495(k,i) -> p$464,p$465,k<0,i<0,p$490,i<k and free(t,i),free(t,k)and free(s,i),k=<i and free(t,s(i)),i<k and free(u,i) [expansion from 358]
 362 + p$464 -> free(u,k)                                  [expansion from 358]
 363 + p$464 -> free(s,i)                                  [expansion from 358]
 364 + p$495(k,i) -> p$463,p$464,p$465,k<0,i<0,p$490,i<k and free(t,i),free(t,k)and free(s,i),k=<i and free(t,s(i)) [expansion from 361]
 365 + p$463 -> i<k                                        [expansion from 361]
 366 + p$463 -> free(u,i)                                  [expansion from 361]
 367 + p$495(k,i) -> p$462,p$463,p$464,p$465,k<0,i<0,p$490,i<k and free(t,i),free(t,k)and free(s,i) [expansion from 364]
 368 + p$462 -> k=<i                                       [expansion from 364]
 369 + p$462 -> free(t,s(i))                               [expansion from 364]
 370 + p$495(k,i) -> p$461,p$462,p$463,p$464,p$465,k<0,i<0,p$490,i<k and free(t,i) [expansion from 367]
 371 + p$461 -> free(t,k)                                  [expansion from 367]
 372 + p$461 -> free(s,i)                                  [expansion from 367]
 373 + p$495(k,i) -> p$460,p$461,p$462,p$463,p$464,p$465,k<0,i<0,p$490 [expansion from 370]
 374 + p$460 -> i<k                                        [expansion from 370]
 375 + p$460 -> free(t,i)                                  [expansion from 370]
 376 + p$498,p$460,p$461,p$462,p$463,p$464,p$465,k<0,i<0,p$490 [negative chaining of 64 from 373]
 377 + p$498,p$460,p$461,p$462,p$463,p$464,p$465,p$490 [reduction of 376 by [189,73,L,L,188,73,L,L]]
 378 + p$498,p$461,p$462,p$463,p$464,p$465,p$490,i<k [negative chaining of 377 from 374]
 379 + p$498,p$461,p$462,p$463,p$464,p$465,p$490,free(t,i) [negative chaining of 377 from 375]
 380 + i<k,p$490,p$465,p$464,p$462,p$461,p$498      [reduction of 378 by [365]]
 381 + p$498,p$462,p$463,p$464,p$465,p$490,p$461,p$471 [negative chaining of 379 from 168]
 382 + p$498,p$463,p$464,p$465,p$490,p$471,p$462,free(t,k) [negative chaining of 381 from 371]
 383 + p$498,p$463,p$464,p$465,p$490,p$471,p$462,free(s,i) [negative chaining of 381 from 372]
 384 + free(s,i),p$462,p$471,p$490,p$465,p$463,p$498 [reduction of 383 by [363]]
 385 + p$477 -> p$462,p$471,p$490,p$465,p$463,p$498,p$484 [negative chaining of 384 from 139]
 386 + p$477 -> p$462,p$471,p$490,p$465,p$463,p$498 [reduction of 385 by [110,L]]
 387 + p$498,p$464,p$465,p$490,p$471,p$463,p$462,p$477 [negative chaining of 382 from 140]
 388 + p$462,p$463,p$471,p$490,p$465,p$464,p$498    [reduction of 387 by [386]]
 389 + p$463,p$471,p$490,p$465,p$464,p$498,k=<i [negative chaining of 388 from 368]
 390 + p$463,p$471,p$490,p$465,p$464,p$498,free(t,s(i)) [negative chaining of 388 from 369]
 391 + k=<i,p$498,p$464,p$490,p$471,p$463           [reduction of 389 by [359]]
 398 + p$471,p$490,p$465,p$464,p$498,p$463,p$470 [negative chaining of 390 from 171]
 401 + p$490,p$498,p$471,p$470,p$465,p$464,free(u,i) [negative chaining of 398 from 366]
 402 + p$490,p$498,p$471,p$470,p$465,p$464        [reduction of 401 by [169,L]]
 403 + p$498,p$490,p$471,p$470,p$465,free(u,k) [negative chaining of 402 from 362]
 404 + p$498,p$490,p$471,p$470,p$465,free(s,i) [negative chaining of 402 from 363]
 405 + p$498,p$490,p$471,p$470,p$465,p$477  [negative chaining of 403 from 141]
 407 + p$498,p$490,p$477,p$471,p$470,free(u,s(i)) [negative chaining of 405 from 360]
 408 + p$498,p$490,p$477,p$471,p$470              [reduction of 407 by [172,L]]
 409 + p$498,p$490,p$477,p$471,i<k,p$476    [negative chaining of 408 from 170]
 410 + p$498,p$490,p$477,p$471,i<k          [reduction of 409 by [142,110,L,L]]
 411 + p$498,p$464,p$490,p$471,p$463,p$498,p$490,p$477,p$471 [chaining of 391 from 410]
 412 + p$464,p$463,p$498,p$490,p$477,p$471                [condensement of 411]
 414 + p$498,p$490,p$477,p$471,p$464,free(u,i) [negative chaining of 412 from 366]
 415 + p$498,p$490,p$477,p$471,p$464              [reduction of 414 by [169,L]]
 416 + p$498,p$490,p$477,p$471,free(u,k)    [negative chaining of 415 from 362]
 418 + p$498,p$490,p$477,p$471                    [reduction of 416 by [141,L]]
 419 + p$498,p$490,p$477,k=<i,p$476         [negative chaining of 418 from 167]
 420 + p$498,p$490,p$477,k=<i               [reduction of 419 by [142,110,L,L]]
 425 + p$490,p$465,p$464,p$462,p$461,p$498,p$498,p$490,p$477 [chaining of 380 from 420]
 427 + p$465,p$464,p$462,p$461,p$498,p$490,p$477          [condensement of 425]
 429 + p$498,p$490,p$477,p$465,p$464,p$462,free(t,k) [negative chaining of 427 from 371]
 431 + p$498,p$490,p$477,p$465,p$464,p$462        [reduction of 429 by [140,L]]
 433 + p$498,p$490,p$477,p$465,p$464,free(t,s(i)) [negative chaining of 431 from 369]
 434 + p$498,p$490,p$477,p$465,p$464,p$470  [negative chaining of 433 from 171]
 436 + p$498,p$490,p$477,p$470,p$465,free(u,k) [negative chaining of 434 from 362]
 438 + p$498,p$490,p$477,p$470,p$465              [reduction of 436 by [141,L]]
 440 + p$498,p$490,p$477,p$470,free(u,s(i)) [negative chaining of 438 from 360]
 441 + p$498,p$490,p$477,p$470                    [reduction of 440 by [172,L]]
 442 + p$498,p$490,p$477,i<k,p$476          [negative chaining of 441 from 170]
 443 + p$498,p$490,p$477              [reduction of 442 by [420,L,142,110,L,L]]
 444 + p$477 -> p$490,p$498,p$471,p$465,p$463,k=<i [negative chaining of 386 from 368]
 446 + k=<i,p$463,p$471,p$498,p$490             [reduction of 444 by [443,359]]
 456 + p$477 -> p$498,p$490,p$471,p$470,p$465,p$484 [negative chaining of 404 from 139]
 457 + p$498,p$490,p$471,p$470,p$465          [reduction of 456 by [443,110,L]]
 459 + p$498,p$490,p$471,p$470,free(u,s(i)) [negative chaining of 457 from 360]
 460 + p$498,p$490,p$471,p$470                    [reduction of 459 by [172,L]]
 461 + p$498,p$490,p$471,i<k,p$476          [negative chaining of 460 from 170]
 462 + p$498,p$490,p$471,i<k                [reduction of 461 by [142,110,L,L]]
 465 + p$463,p$471,p$498,p$490,p$498,p$490,p$471     [chaining of 446 from 462]
 468 + p$463,p$498,p$490,p$471                            [condensement of 465]
 470 + p$498,p$490,p$471,free(u,i)          [negative chaining of 468 from 366]
 471 + p$498,p$490,p$471                          [reduction of 470 by [169,L]]
 472 + p$498,p$490,k=<i,p$476               [negative chaining of 471 from 167]
 473 + p$498,p$490,k=<i                     [reduction of 472 by [142,110,L,L]]
 478 + p$490,p$465,p$464,p$462,p$461,p$498,p$498,p$490 [chaining of 380 from 473]
 481 + p$465,p$464,p$462,p$461,p$498,p$490                [condensement of 478]
 485 + p$498,p$490,p$465,p$464,p$462,free(s,i) [negative chaining of 481 from 372]
 486 + p$498,p$490,p$465,p$464,p$462    [reduction of 485 by [139,110,L,443,L]]
 488 + p$498,p$490,p$465,p$464,free(t,s(i)) [negative chaining of 486 from 369]
 489 + p$498,p$490,p$465,p$464,p$470        [negative chaining of 488 from 171]
 492 + p$498,p$490,p$470,p$465,free(s,i)    [negative chaining of 489 from 363]
 493 + p$498,p$490,p$470,p$465          [reduction of 492 by [139,110,L,443,L]]
 495 + p$498,p$490,p$470,free(u,s(i))       [negative chaining of 493 from 360]
 496 + p$498,p$490,p$470                          [reduction of 495 by [172,L]]
 497 + p$498,p$490,i<k,p$476                [negative chaining of 496 from 170]
 498 + p$498,p$490                    [reduction of 497 by [473,L,142,110,L,L]]
 499 + p$459,p$495(k,i) -> k<0,i<0,p$478                   [expansion from 353]
 500 + free(t,k)and free(s,i) -> p$459                     [expansion from 353]
 501 + i<k and free(t,i)or k=<i and free(t,s(i)) -> p$459  [expansion from 353]
 502 + free(t,k),free(s,i) -> p$459                        [expansion from 500]
 503 + p$458,p$495(k,i) -> k<0,i<0,p$478                   [expansion from 354]
 504 + free(u,k)and free(s,i) -> p$458                     [expansion from 354]
 505 + i<k and free(u,i)or k=<i and free(u,s(i)) -> p$458  [expansion from 354]
 506 + free(u,k),free(s,i) -> p$458                        [expansion from 504]
 507 + p$457 -> p$459                                      [expansion from 501]
 508 + i<k and free(t,i) -> p$457                          [expansion from 501]
 509 + k=<i and free(t,s(i)) -> p$457                      [expansion from 501]
 510 + i<k,free(t,i) -> p$457                              [expansion from 508]
 511 + free(t,i) -> k=<i,p$457                   [totality resolution from 510]
 512 + k=<i,free(t,s(i)) -> p$457                          [expansion from 509]
 513 + free(t,s(i)) -> i<k,p$457                 [totality resolution from 512]
 514 + p$456 -> p$458                                      [expansion from 505]
 515 + i<k and free(u,i) -> p$456                          [expansion from 505]
 516 + k=<i and free(u,s(i)) -> p$456                      [expansion from 505]
 517 + i<k,free(u,i) -> p$456                              [expansion from 515]
 518 + free(u,i) -> k=<i,p$456                   [totality resolution from 517]
 519 + k=<i,free(u,s(i)) -> p$456                          [expansion from 516]
 520 + free(u,s(i)) -> i<k,p$456                 [totality resolution from 519]
 527 + p$459 -> p$498,p$478,k<0,i<0          [negative chaining of 64 from 499]
 528 + p$459 -> p$498 [reduction of 527 by [136,106,73,L,498,L,L,189,73,L,L,188,73,L,L]]
 529 + p$458 -> p$498,p$478,k<0,i<0          [negative chaining of 64 from 503]
 530 + p$458 -> p$498 [reduction of 529 by [136,106,73,L,498,L,L,189,73,L,L,188,73,L,L]]
 532 + p$485,p$479,p$472,free(t,i),k=<i,p$456 [negative chaining of 196 from 518]
 534 + p$485,p$479,p$472,free(t,i),p$456          [reduction of 532 by [195,L]]
 565 + p$485,p$479,p$472,p$456,k=<i,p$457   [negative chaining of 534 from 511]
 566 + p$485,p$479,p$472,p$456,p$457              [reduction of 565 by [195,L]]
 567 + p$485,p$479,p$472,p$457,p$458        [negative chaining of 566 from 514]
 568 + p$485,p$479,p$472,p$458,p$459        [negative chaining of 567 from 507]
 569 + p$485,p$479,p$472,p$459,p$498        [negative chaining of 568 from 530]
 570 + p$479,p$472,p$498           [reduction of 569 by [106,73,L,498,L,528,L]]
 571 + p$498,p$479,free(s,i)                [negative chaining of 570 from 165]
 572 + p$498,p$479,free(u,k),free(t,k)      [negative chaining of 570 from 166]
 573 + p$498,p$479      [reduction of 572 by [506,530,L,571,L,502,528,L,571,L]]
 574 + p$498,k=<i                           [negative chaining of 573 from 133]
 575 + p$498,free(u,s(i)),free(t,s(i))      [negative chaining of 573 from 135]
 576 + p$498 [reduction of 575 by [520,514,530,L,L,574,L,L,513,507,528,L,L,574,L,L]]
 577 + p$499 ->                                     [reduction of 352 by [576]]
 578 + free(subst(t,A,B),C)==(free(t,A)and free(B,C)or(C<A and free(t,C)or A=<C and free(t,s(C)))),C<0,A<0 [reduction of 52 by [577,L]]
 579 + p$497 ->                                    [reduction of 57 by [577,L]]
 580 + p$489,p$492 ->                              [reduction of 92 by [579,L]]
 582 + 0=<i                                       [reduction of 186 by [579,L]]
 583 + 0=<k                                       [reduction of 187 by [579,L]]
 590 + free(t,s(k))and free(lift(s,0),s(i))or(s(i)<s(k)and free(t,s(i))or s(k)=<s(i)and free(t,s(s(i)))),p$492,s(i)<0,s(k)<0 [chaining of 81 from 578]
 593 + free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0)or(s(i)<s(k)and free(t,s(i))or s(k)=<s(i)and free(t,s(s(i)))),p$492 [reduction of 590 by [45,9,11,582,L,11,583,L]]
 594 + p$455,p$492                                         [expansion from 593]
 595 + p$455 -> free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0),s(i)<s(k)and free(t,s(i))or s(k)=<s(i)and free(t,s(s(i))) [expansion from 593]
 596 + p$455 -> free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0),s(i)<s(k)and free(t,s(i)),s(k)=<s(i)and free(t,s(s(i))) [expansion from 595]
 597 + p$492,s(k)=<s(i)and free(t,s(s(i))),s(i)<s(k)and free(t,s(i)),free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0) [negative chaining of 594 from 596]
 598 + p$454,p$492,s(i)<s(k)and free(t,s(i)),free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0) [expansion from 597]
 599 + p$454 -> s(k)=<s(i)                                 [expansion from 597]
 600 + p$454 -> free(t,s(s(i)))                            [expansion from 597]
 601 + p$453,p$492,p$454,s(i)<s(k)and free(t,s(i))         [expansion from 598]
 602 + p$453 -> free(t,s(k))                               [expansion from 598]
 603 + p$453 -> free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0 [expansion from 598]
 604 + p$453 -> free(s,i)and 0<s(i),free(s,s(i))and s(i)<0 [expansion from 603]
 605 + p$452,p$492,p$454,p$453                             [expansion from 601]
 606 + p$452 -> s(i)<s(k)                                  [expansion from 601]
 607 + p$452 -> free(t,s(i))                               [expansion from 601]
 608 + p$492,p$454,p$453,s(i)<s(k)          [negative chaining of 605 from 606]
 609 + p$492,p$454,p$453,free(t,s(i))       [negative chaining of 605 from 607]
 610 + s(i)<A,A=<k,p$492,p$454,p$453                  [chaining of 33 from 608]
 613 + p$453,p$454,p$492,s(i)=<k                [variable elimination from 610]
 614 + i<k,p$454,p$492,p$453                          [chaining of 11 from 613]
 619 + p$492,p$454,p$453,k=<i,p$482         [negative chaining of 609 from 121]
 621 + p$492,p$454,p$453               [reduction of 619 by [614,L,117,96,L,L]]
 622 + p$492,p$454,free(t,s(k))             [negative chaining of 621 from 602]
 624 + free(s,i) -> p$492,p$454,p$488        [negative chaining of 622 from 99]
 625 + free(s,i) -> p$492,p$454                    [reduction of 624 by [96,L]]
 627 + p$492,p$454,free(s,s(i))and s(i)<0,free(s,i)and 0<s(i) [negative chaining of 621 from 604]
 629 + p$492,p$454,free(s,s(i))and s(i)<0       [reduction of 627 by [625,L,L]]
 630 + p$451,p$492,p$454                                   [expansion from 629]
 632 + p$451 -> s(i)<0                                     [expansion from 629]
 633 + p$451 ->                                [reduction of 632 by [11,582,L]]
 634 + p$454,p$492                                [reduction of 630 by [633,L]]
 635 + p$492,s(k)=<s(i)                     [negative chaining of 634 from 599]
 639 + s(A)=s(i) -> s(k)=s(i),k<A,p$492               [chaining of 40 from 635]
 641 + A=i -> p$492,k<A,k=i                         [reduction of 639 by [7,7]]
 642 + p$492,k<i,k=i                            [variable elimination from 641]
 643 + k=<i,p$492                                         [condensement of 642]
 656 + p$492,free(t,s(s(i)))                [negative chaining of 634 from 600]
 657 + p$492                     [reduction of 656 by [123,117,96,L,L,643,L,L]]
 658 + p$489 ->                                     [reduction of 580 by [657]]
 659 + free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0)or(s(i)<s(k)and free(t,s(i))or s(k)=<s(i)and free(t,s(s(i)))) ->  [reduction of 94 by [578,11,583,L,11,582,L,45,11,582,L,9,658,L]]
 661 + free(t,s(i)),p$475,p$483                   [reduction of 194 by [658,L]]
 662 + i<k,p$475,p$483                            [reduction of 193 by [658,L]]
 663 + free(t,s(k))and(free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0) ->  [expansion from 659]
 664 + s(i)<s(k)and free(t,s(i))or s(k)=<s(i)and free(t,s(s(i))) ->  [expansion from 659]
 665 + free(t,s(k)),free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0 ->  [expansion from 663]
 666 + s(i)<s(k)and free(t,s(i)) ->                        [expansion from 664]
 667 + s(k)=<s(i)and free(t,s(s(i))) ->                    [expansion from 664]
 668 + s(i)<s(k),free(t,s(i)) ->                           [expansion from 666]
 669 + free(t,s(i)) -> s(k)=<s(i)                [totality resolution from 668]
 670 + s(k)=<s(i),free(t,s(s(i))) ->                       [expansion from 667]
 671 + free(t,s(s(i))) -> s(i)<s(k)              [totality resolution from 670]
 676 + p$475,p$483,k=<i,p$482               [negative chaining of 661 from 121]
 678 + p$475,p$483,s(k)=<s(i)               [negative chaining of 661 from 669]
 679 + p$475,p$483,p$482                          [reduction of 676 by [662,L]]
 680 + p$475,p$483,k=i                       [reduction of 678 by [40,662,L,7]]
 681 + p$483,p$482,free(s,i)                [negative chaining of 679 from 151]
 682 + p$483,p$482,free(t,s(k))             [negative chaining of 679 from 150]
 692 + free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0 -> p$483,p$482 [negative chaining of 682 from 665]
 693 + 0<s(i)or free(s,s(i))and s(i)<0 -> p$482,p$483 [reduction of 692 by [681,L]]
 695 + 0<s(i) -> p$450                                     [expansion from 693]
 697 + s(i)=<0,p$450                             [totality resolution from 695]
 698 + p$450,s(i)=0                              [reduction of 697 by [11,582]]
 701 + i<0,p$450                                      [chaining of 11 from 698]
 720 + p$450                                      [reduction of 701 by [582,L]]
 749 + p$475,p$483,p$483,p$475                       [chaining of 662 from 680]
 755 + p$483,p$475                                        [condensement of 749]
 758 + p$483,free(s,i)                      [negative chaining of 755 from 151]
 759 + p$483,free(t,s(k))                   [negative chaining of 755 from 150]
 760 + free(s,i)and 0<s(i)or free(s,s(i))and s(i)<0 -> p$483 [negative chaining of 759 from 665]
 762 + 0<s(i)or free(s,s(i))and s(i)<0 -> p$483   [reduction of 760 by [758,L]]
 764 + p$450 -> p$483                                      [expansion from 762]
 765 + p$483                                        [reduction of 764 by [720]]
 766 + k=<i                                         [reduction of 115 by [765]]
 767 + false                       [reduction of 116 by [765,671,40,766,L,L,L]]

Length = 426, Depth = 131



Total time: 448980 milliseconds

Number of forward inferences: 354
Number of tableau inferences: 157
Number of kept clauses: 436
*/