use(subst).
use(int).
use(beta).
use(lemmaB1).
use(lemmaF3).

lemmaF3(S,T,K,I).

%Induktionsanfang der Induktion ueber beta

lemmaB1(app(abs(s),t),subst(s,0,t),i),

%2 Induktionsschritte

((lemmaB1(s,t,i) and beta(s,t)) =>
 (lemmaB1(app(s,u),app(t,u),i) and lemmaB1(app(u,s),app(u,t),i))),

((all(I,lemmaB1(s,t,I)) and beta(s,t)) => lemmaB1(abs(s),abs(t),i)) -> [].


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

/*
Proof:
======

  24 : free(app(A,B),C)==(free(A,C)or free(B,C))                        [input]
  25 : free(abs(A),B)==free(A,s(B))                                     [input]
  36 : A<s(A)                                                           [input]
  39 : beta(app(abs(A),B),subst(A,0,B))                                 [input]
  46 : lemmaB1(A,B,C)==(0=<C=>beta(A,B)=>free(B,C)=>free(A,C))          [input]
  47 : 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]
  48 : lemmaF3(A,B,C,D)                                                 [input]
  49 : lemmaB1(app(abs(s),t),subst(s,0,t),i),lemmaB1(s,t,i)and beta(s,t)=>lemmaB1(app(s,u),app(t,u),i)and lemmaB1(app(u,s),app(u,t),i),!A.(lemmaB1(s,t,A)) and beta(s,t)=>lemmaB1(abs(s),abs(t),i) ->  [input]
  61 : 0=<A and 0=<B=>free(subst(C,B,D),A)<=>free(C,B)and free(D,A)or(A<B and free(C,A)or B=<A and free(C,s(A))) [reduction of 48 by [47]]
  62 : 0=<A,0=<B -> free(subst(C,B,D),A)==(free(C,B)and free(D,A)or(A<B and free(C,A)or B=<A and free(C,s(A)))) [expansion from 61]
  64 : A<0,B<0,free(subst(C,A,D),B)==(free(C,A)and free(D,B)or(B<A and free(C,B)or A=<B and free(C,s(B)))) [totality resolution from 62]
  65 : (0=<i=>beta(s,t)=>free(t,i)=>free(s,i))and beta(s,t)=>(0=<i=>beta(app(s,u),app(t,u))=>free(t,i)or free(u,i)=>free(s,i)or free(u,i))and(0=<i=>beta(app(u,s),app(u,t))=>free(u,i)or free(t,i)=>free(u,i)or free(s,i)),0=<i=>free(subst(s,0,t),i)=>free(s,s(i))or free(t,i),!A.(0=<A=>beta(s,t)=>free(t,A)=>free(s,A)) and beta(s,t)=>0=<i=>beta(abs(s),abs(t))=>free(t,s(i))=>free(s,s(i)) ->  [reduction of 49 by [46,24,25,39,L,46,24,24,46,24,24,46,46,25,25,46]]
  66 : p$199,!A.(0=<A=>beta(s,t)=>free(t,A)=>free(s,A)) and beta(s,t)=>0=<i=>beta(abs(s),abs(t))=>free(t,s(i))=>free(s,s(i)),(0=<i=>beta(s,t)=>free(t,i)=>free(s,i))and beta(s,t)=>(0=<i=>beta(app(s,u),app(t,u))=>free(t,i)or free(u,i)=>free(s,i)or free(u,i))and(0=<i=>beta(app(u,s),app(u,t))=>free(u,i)or free(t,i)=>free(u,i)or free(s,i)) ->  [expansion from 65]
  67 : p$199,0=<i                                           [expansion from 65]
  68 : free(subst(s,0,t),i)=>free(s,s(i))or free(t,i) -> p$199 [expansion from 65]
  69 : free(s,0)and free(t,i)or(i<0 and free(s,i)or 0=<i and free(s,s(i)))=>free(s,s(i))or free(t,i) -> p$199 [reduction of 68 by [64,67,L]]
  70 : p$198,!A.(0=<A=>beta(s,t)=>free(t,A)=>free(s,A)) and beta(s,t)=>0=<i=>beta(abs(s),abs(t))=>free(t,s(i))=>free(s,s(i)),p$199 ->  [expansion from 66]
  71 : p$198,(0=<i=>beta(s,t)=>free(t,i)=>free(s,i))and beta(s,t) [expansion from 66]
  72 : (0=<i=>beta(app(s,u),app(t,u))=>free(t,i)or free(u,i)=>free(s,i)or free(u,i))and(0=<i=>beta(app(u,s),app(u,t))=>free(u,i)or free(t,i)=>free(u,i)or free(s,i)) -> p$198 [expansion from 66]
  73 : 0=<i=>beta(app(s,u),app(t,u))=>free(t,i)or free(u,i)=>free(s,i)or free(u,i),0=<i=>beta(app(u,s),app(u,t))=>free(u,i)or free(t,i)=>free(u,i)or free(s,i) -> p$198 [expansion from 72]
  74 : p$197 -> p$199                                       [expansion from 69]
  75 : p$197,free(s,0)and free(t,i)or(i<0 and free(s,i)or 0=<i and free(s,s(i))) [expansion from 69]
  76 : free(s,s(i))or free(t,i) -> p$197                    [expansion from 69]
  77 : p$197,free(s,0)and free(t,i),i<0 and free(s,i),0=<i and free(s,s(i)) [expansion from 75]
  78 : p$196,p$198,p$199 ->                                 [expansion from 70]
  79 : p$196,!A.(0=<A=>beta(s,t)=>free(t,A)=>free(s,A)) and beta(s,t) [expansion from 70]
  80 : 0=<i=>beta(abs(s),abs(t))=>free(t,s(i))=>free(s,s(i)) -> p$196 [expansion from 70]
  81 : p$195,p$198                                          [expansion from 71]
  82 : p$195 -> 0=<i=>beta(s,t)=>free(t,i)=>free(s,i)       [expansion from 71]
  83 : p$195 -> beta(s,t)                                   [expansion from 71]
  84 : p$195,0=<i,beta(s,t),free(t,i) -> free(s,i)          [expansion from 82]
  85 : p$195,beta(s,t),free(t,i) -> i<0,free(s,i) [totality resolution from 84]
  86 : p$194,0=<i=>beta(app(s,u),app(t,u))=>free(t,i)or free(u,i)=>free(s,i)or free(u,i) -> p$198 [expansion from 73]
  87 : p$194,0=<i                                           [expansion from 73]
  88 : beta(app(u,s),app(u,t))=>free(u,i)or free(t,i)=>free(u,i)or free(s,i) -> p$194 [expansion from 73]
  89 : p$193,p$197,i<0 and free(s,i),0=<i and free(s,s(i))  [expansion from 77]
  91 : p$193 -> free(t,i)                                   [expansion from 77]
  92 : p$192 -> p$197                                       [expansion from 76]
  93 : free(s,s(i)) -> p$192                                [expansion from 76]
  94 : free(t,i) -> p$192                                   [expansion from 76]
  95 : p$191,p$196                                          [expansion from 79]
  96 : p$191 -> !A.(0=<A=>beta(s,t)=>free(t,A)=>free(s,A))  [expansion from 79]
  97 : p$191 -> beta(s,t)                                   [expansion from 79]
  98 : p$191,0=<A,beta(s,t),free(t,A) -> free(s,A)          [expansion from 96]
  99 : p$191,beta(s,t),free(t,A) -> A<0,free(s,A) [totality resolution from 98]
 100 : p$190 -> p$196                                       [expansion from 80]
 101 : p$190,0=<i                                           [expansion from 80]
 102 : beta(abs(s),abs(t))=>free(t,s(i))=>free(s,s(i)) -> p$190 [expansion from 80]
 103 : p$189,p$194 -> p$198                                 [expansion from 86]
 104 : p$189,0=<i                                           [expansion from 86]
 105 : beta(app(s,u),app(t,u))=>free(t,i)or free(u,i)=>free(s,i)or free(u,i) -> p$189 [expansion from 86]
 106 : p$188 -> p$194                                       [expansion from 88]
 108 : free(u,i)or free(t,i)=>free(u,i)or free(s,i) -> p$188 [expansion from 88]
 109 : p$187,p$197,p$193,i<0 and free(s,i)                  [expansion from 89]
 111 : p$187 -> free(s,s(i))                                [expansion from 89]
 112 : p$186 -> p$190                                      [expansion from 102]
 114 : free(t,s(i))=>free(s,s(i)) -> p$186                 [expansion from 102]
 115 : p$185 -> p$189                                      [expansion from 105]
 117 : free(t,i)or free(u,i)=>free(s,i)or free(u,i) -> p$185 [expansion from 105]
 118 : p$184 -> p$188                                      [expansion from 108]
 119 : p$184,free(u,i)or free(t,i)                         [expansion from 108]
 120 : free(u,i)or free(s,i) -> p$184                      [expansion from 108]
 121 : p$184,free(u,i),free(t,i)                           [expansion from 119]
 122 : p$183,p$197,p$193,p$187                             [expansion from 109]
 123 : p$183 -> i<0                                        [expansion from 109]
 125 : p$182 -> p$186                                      [expansion from 114]
 126 : p$182,free(t,s(i))                                  [expansion from 114]
 127 : free(s,s(i)) -> p$182                               [expansion from 114]
 128 : p$181 -> p$185                                      [expansion from 117]
 129 : p$181,free(t,i)or free(u,i)                         [expansion from 117]
 130 : free(s,i)or free(u,i) -> p$181                      [expansion from 117]
 131 : p$181,free(t,i),free(u,i)                           [expansion from 129]
 132 : p$180 -> p$184                                      [expansion from 120]
 133 : free(u,i) -> p$180                                  [expansion from 120]
 134 : free(s,i) -> p$180                                  [expansion from 120]
 135 : p$179 -> p$181                                      [expansion from 130]
 136 : free(s,i) -> p$179                                  [expansion from 130]
 137 : free(u,i) -> p$179                                  [expansion from 130]
 138 : p$198,beta(s,t)                        [negative chaining of 81 from 83]
 139 : p$196,beta(s,t)                        [negative chaining of 95 from 97]
 145 : p$184,free(t,i),p$180                [negative chaining of 121 from 133]
 147 : p$184,free(t,i)                            [reduction of 145 by [132,L]]
 152 : p$197,p$193,p$187,i<0                [negative chaining of 122 from 123]
 155 : p$181,free(t,i),p$179                [negative chaining of 131 from 137]
 156 : p$181,free(t,i)                            [reduction of 155 by [135,L]]
 164 : p$199,p$197,p$193,p$187                        [chaining of 67 from 152]
 168 : p$199,p$187,p$193                           [reduction of 164 by [74,L]]
 171 : p$199,p$193,free(s,s(i))             [negative chaining of 168 from 111]
 172 : p$199,p$193                       [reduction of 171 by [93,92,74,L,L,L]]
 174 : p$199,free(t,i)                       [negative chaining of 172 from 91]
 175 : p$199                             [reduction of 174 by [94,92,74,L,L,L]]
 176 : p$196,p$198 ->                                [reduction of 78 by [175]]
 178 : free(t,i),p$195 -> p$198,i<0,free(s,i) [negative chaining of 138 from 85]
 179 : free(t,i),p$195 -> p$196,i<0,free(s,i) [negative chaining of 139 from 85]
 180 : free(t,i) -> free(s,i),i<0,p$198              [reduction of 178 by [81]]
 181 : free(t,i),p$195 -> free(s,i),i<0       [reduction of 179 by [176,180,L]]
 182 : p$195 -> p$184,free(s,i),i<0         [negative chaining of 147 from 181]
 183 : p$195 -> p$181,free(s,i),i<0         [negative chaining of 156 from 181]
 185 : p$195 -> p$184,i<0                   [reduction of 182 by [134,132,L,L]]
 186 : p$195 -> p$181,i<0                   [reduction of 183 by [136,135,L,L]]
 187 : p$198,i<0,p$184                       [negative chaining of 81 from 185]
 188 : p$198,i<0,p$181                       [negative chaining of 81 from 186]
 189 : p$194,p$198,p$184                              [chaining of 87 from 187]
 192 : p$194,p$198                          [reduction of 189 by [118,106,L,L]]
 198 : p$189,p$198,p$181                             [chaining of 104 from 188]
 200 : p$198            [reduction of 198 by [103,192,L,128,115,103,192,L,L,L]]
 201 : p$196 ->                                     [reduction of 176 by [200]]
 202 : p$190 ->                                   [reduction of 100 by [201,L]]
 203 : p$191                                       [reduction of 95 by [201,L]]
 204 : beta(s,t)                                  [reduction of 139 by [201,L]]
 206 : free(t,A) -> free(s,A),A<0                [reduction of 99 by [204,203]]
 207 : p$186 ->                                   [reduction of 112 by [202,L]]
 208 : 0=<i                                       [reduction of 101 by [202,L]]
 210 : p$182 ->                                   [reduction of 125 by [207,L]]
 214 : free(s,s(i)) ->                            [reduction of 127 by [210,L]]
 215 : false                 [reduction of 126 by [206,36,208,L,214,L,L,210,L]]

Length = 116, Depth = 31



Total time: 43680 milliseconds

Number of forward inferences: 47
Number of tableau inferences: 63
Number of kept clauses: 161
*/