use(subst).
use(int).
use(pbeta).
use(lemmaP1).
use(lemmaP2).
use(subst_lemmas).

lemmaP1(S,T,I).
lemma5(T,U,V,I,J).

% Proof by induction over pbeta:

goal

%Induktionsanfang

(0=<k => lemmaP2(s,t,var(k),var(k),i)),

%Drei Induktionsschritte

((all(I,all(S,all(T,lemmaP2(S,T,u,v,I)))) and pbeta(u,v))
  => lemmaP2(s,t,abs(u),abs(v),i)),

((lemmaP2(s,t,u,v,i) and lemmaP2(s,t,w,x,i) and pbeta(u,v) and pbeta(w,x))
  => lemmaP2(s,t,app(u,w),app(v,x),i)),

((all(I,all(S,all(T,lemmaP2(S,T,u,v,I) and lemmaP2(S,T,w,x,I))))
  and pbeta(u,v) and pbeta(w,x))
  => lemmaP2(s,t,app(abs(u),w),subst(v,0,x),i)) -> [].

top_predicates_precedence([lemmaP2,lemmaP1,lemma5]).
option([var_overlaps(off),search_depth(1)]).


/*
Proof:
======

  11 : A<s(A)                                                           [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]
  36 : A<s(A)                                                           [input]
  40 : pbeta(A,B) -> pbeta(abs(A),abs(B))                               [input]
  41 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(A,C),app(B,D))               [input]
  42 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(abs(A),C),subst(B,0,D))      [input]
  43 : pbeta(A,A)                                                       [input]
  44 : lemmaP1(A,B,C)==(0=<C and pbeta(A,B)=>pbeta(lift(A,C),lift(B,C))) [input]
  45 : lemmaP2(A,B,C,D,E)==(0=<E and pbeta(A,B)and pbeta(C,D)=>pbeta(subst(C,E,A),subst(D,E,B))) [input]
  50 : lemma5(A,B,C,D,E)==(D<s(E)and 0=<D=>subst(subst(A,s(E),lift(C,D)),D,subst(B,E,C))=subst(subst(A,D,B),E,C)) [input]
  53 : lemmaP1(A,B,C)                                                   [input]
  54 : lemma5(A,B,C,D,E)                                                [input]
  55 + 0=<k=>lemmaP2(s,t,var(k),var(k),i),!A,B,C.(lemmaP2(B,C,u,v,A)) and pbeta(u,v)=>lemmaP2(s,t,abs(u),abs(v),i),lemmaP2(s,t,u,v,i)and lemmaP2(s,t,w,x,i)and pbeta(u,v)and pbeta(w,x)=>lemmaP2(s,t,app(u,w),app(v,x),i),!D,E,F.(lemmaP2(E,F,u,v,D)and lemmaP2(E,F,w,x,D)) and pbeta(u,v)and pbeta(w,x)=>lemmaP2(s,t,app(abs(u),w),subst(v,0,x),i) ->  [input]
  58 : A=<B,subst(var(A),B,C)=var(p(A))           [totality resolution from 14]
  59 : A=<B,subst(var(B),A,C)=var(B)              [totality resolution from 16]
  67 : pbeta(A,B),pbeta(C,D) -> pbeta(app(A,C),app(B,D))    [expansion from 41]
  68 : pbeta(A,B),pbeta(C,D) -> pbeta(app(abs(A),C),subst(B,0,D)) [expansion from 42]
  69 : 0=<A and pbeta(B,C)=>pbeta(lift(B,A),lift(C,A)) [reduction of 53 by [44]]
  70 : 0=<A,pbeta(B,C) -> pbeta(lift(B,A),lift(C,A))        [expansion from 69]
  71 : pbeta(A,B) -> C<0,pbeta(lift(A,C),lift(B,C)) [totality resolution from 70]
  72 : A<s(B)and 0=<A=>subst(subst(C,s(B),lift(D,A)),A,subst(E,B,D))=subst(subst(C,A,E),B,D) [reduction of 54 by [50]]
  73 : A<s(B),0=<A -> subst(subst(C,s(B),lift(D,A)),A,subst(E,B,D))=subst(subst(C,A,E),B,D) [expansion from 72]
  75 : A<0,s(B)=<A,subst(subst(C,s(B),lift(D,A)),A,subst(E,B,D))=subst(subst(C,A,E),B,D) [totality resolution from 73]
  76 + (0=<i and pbeta(s,t)and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i and pbeta(s,t)and pbeta(w,x)=>pbeta(subst(w,i,s),subst(x,i,t)))and pbeta(u,v)and pbeta(w,x)=>0=<i and pbeta(s,t)and pbeta(app(u,w),app(v,x))=>pbeta(app(subst(u,i,s),subst(w,i,s)),app(subst(v,i,t),subst(x,i,t))),!A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) and pbeta(u,v)=>0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))=>pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))),0=<k=>0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)),!D,E,F.((0=<D and pbeta(E,F)and pbeta(u,v)=>pbeta(subst(u,D,E),subst(v,D,F)))and(0=<D and pbeta(E,F)and pbeta(w,x)=>pbeta(subst(w,D,E),subst(x,D,F)))) and pbeta(u,v)and pbeta(w,x)=>0=<i and pbeta(s,t)and pbeta(app(abs(u),w),subst(v,0,x))=>pbeta(app(abs(subst(u,s(i),lift(s,0))),subst(w,i,s)),subst(subst(v,0,x),i,t)) ->  [reduction of 55 by [45,43,L,45,18,18,45,45,17,17,45,45,45,17,18,45,45]]
  77 + p$499,!A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) and pbeta(u,v)=>0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))=>pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))),0=<k=>0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)),(0=<i and pbeta(s,t)and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i and pbeta(s,t)and pbeta(w,x)=>pbeta(subst(w,i,s),subst(x,i,t)))and pbeta(u,v)and pbeta(w,x)=>0=<i and pbeta(s,t)and pbeta(app(u,w),app(v,x))=>pbeta(app(subst(u,i,s),subst(w,i,s)),app(subst(v,i,t),subst(x,i,t))) ->  [expansion from 76]
  78 + p$499,!A,B,C.((0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)and pbeta(w,x)=>pbeta(subst(w,A,B),subst(x,A,C)))) and pbeta(u,v)and pbeta(w,x) [expansion from 76]
  79 + 0=<i and pbeta(s,t)and pbeta(app(abs(u),w),subst(v,0,x))=>pbeta(app(abs(subst(u,s(i),lift(s,0))),subst(w,i,s)),subst(subst(v,0,x),i,t)) -> p$499 [expansion from 76]
  80 + p$498,!A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) and pbeta(u,v)=>0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))=>pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))),0=<k=>0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)),p$499 ->  [expansion from 77]
  81 + p$498,(0=<i and pbeta(s,t)and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i and pbeta(s,t)and pbeta(w,x)=>pbeta(subst(w,i,s),subst(x,i,t)))and pbeta(u,v)and pbeta(w,x) [expansion from 77]
  82 + 0=<i and pbeta(s,t)and pbeta(app(u,w),app(v,x))=>pbeta(app(subst(u,i,s),subst(w,i,s)),app(subst(v,i,t),subst(x,i,t))) -> p$498 [expansion from 77]
  83 + p$497,p$499                                          [expansion from 78]
  84 + p$497 -> !A,B,C.((0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)and pbeta(w,x)=>pbeta(subst(w,A,B),subst(x,A,C)))) and pbeta(u,v) [expansion from 78]
  85 + p$497 -> pbeta(w,x)                                  [expansion from 78]
  86 + p$496 -> p$499                                       [expansion from 79]
  87 + p$496,0=<i and pbeta(s,t)and pbeta(app(abs(u),w),subst(v,0,x)) [expansion from 79]
  88 + pbeta(app(abs(subst(u,s(i),lift(s,0))),subst(w,i,s)),subst(subst(v,0,x),i,t)) -> p$496 [expansion from 79]
  89 + p$495,p$498                                          [expansion from 81]
  90 + p$495 -> (0=<i and pbeta(s,t)and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i and pbeta(s,t)and pbeta(w,x)=>pbeta(subst(w,i,s),subst(x,i,t)))and pbeta(u,v) [expansion from 81]
  91 + p$495 -> pbeta(w,x)                                  [expansion from 81]
  92 + p$494 -> p$498                                       [expansion from 82]
  93 + p$494,0=<i and pbeta(s,t)and pbeta(app(u,w),app(v,x)) [expansion from 82]
  94 + pbeta(app(subst(u,i,s),subst(w,i,s)),app(subst(v,i,t),subst(x,i,t))) -> p$494 [expansion from 82]
  95 + p$493,p$496                                          [expansion from 87]
  96 + p$493 -> 0=<i and pbeta(s,t)                         [expansion from 87]
  98 + p$492,p$494                                          [expansion from 93]
  99 + p$492 -> 0=<i and pbeta(s,t)                         [expansion from 93]
 101 + p$499,pbeta(w,x)                       [negative chaining of 83 from 85]
 102 + p$498,pbeta(w,x)                       [negative chaining of 89 from 91]
 109 + p$496,0=<i and pbeta(s,t)              [negative chaining of 95 from 96]
 110 + p$491,p$496                                         [expansion from 109]
 111 + p$491 -> 0=<i                                       [expansion from 109]
 112 + p$491 -> pbeta(s,t)                                 [expansion from 109]
 113 + p$496,0=<i                           [negative chaining of 110 from 111]
 114 + p$496,pbeta(s,t)                     [negative chaining of 110 from 112]
 115 + p$494,0=<i and pbeta(s,t)              [negative chaining of 98 from 99]
 116 + p$491,p$494                                         [expansion from 115]
 117 + p$494,0=<i                           [negative chaining of 116 from 111]
 118 + p$494,pbeta(s,t)                     [negative chaining of 116 from 112]
 127 + pbeta(subst(u,i,s),subst(v,i,t)),pbeta(subst(w,i,s),subst(x,i,t)) -> p$494 [negative chaining of 67 from 94]
 142 + p$498,(0=<i and pbeta(s,t)and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i and pbeta(s,t)and pbeta(w,x)=>pbeta(subst(w,i,s),subst(x,i,t)))and pbeta(u,v) [negative chaining of 89 from 90]
 143 + p$498,(0=<i and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i=>pbeta(subst(w,i,s),subst(x,i,t)))and pbeta(u,v) [reduction of 142 by [102,118,92,L,L,L,118,92,L,L]]
 144 + p$490,p$498                                         [expansion from 143]
 145 + p$490 -> (0=<i and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i=>pbeta(subst(w,i,s),subst(x,i,t))) [expansion from 143]
 146 + p$490 -> pbeta(u,v)                                 [expansion from 143]
 147 + p$498,pbeta(u,v)                     [negative chaining of 144 from 146]
 148 + p$498,(0=<i and pbeta(u,v)=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i=>pbeta(subst(w,i,s),subst(x,i,t))) [negative chaining of 144 from 145]
 149 + p$498,(0=<i=>pbeta(subst(u,i,s),subst(v,i,t)))and(0=<i=>pbeta(subst(w,i,s),subst(x,i,t))) [reduction of 148 by [147,L]]
 150 + p$489,p$498                                         [expansion from 149]
 151 + p$489 -> 0=<i=>pbeta(subst(u,i,s),subst(v,i,t))     [expansion from 149]
 152 + p$489 -> 0=<i=>pbeta(subst(w,i,s),subst(x,i,t))     [expansion from 149]
 153 + p$489,0=<i -> pbeta(subst(u,i,s),subst(v,i,t))      [expansion from 151]
 154 + p$489 -> i<0,pbeta(subst(u,i,s),subst(v,i,t)) [totality resolution from 153]
 155 + p$489,0=<i -> pbeta(subst(w,i,s),subst(x,i,t))      [expansion from 152]
 156 + p$489 -> i<0,pbeta(subst(w,i,s),subst(x,i,t)) [totality resolution from 155]
 157 + p$498,pbeta(subst(u,i,s),subst(v,i,t)),i<0 [negative chaining of 150 from 154]
 158 + p$498,pbeta(subst(u,i,s),subst(v,i,t)) [reduction of 157 by [117,92,L,L]]
 159 + p$498,pbeta(subst(w,i,s),subst(x,i,t)),i<0 [negative chaining of 150 from 156]
 160 + p$498                  [reduction of 159 by [127,92,L,158,L,117,92,L,L]]
 161 + !A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) and pbeta(u,v)=>0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))=>pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))),0=<k=>0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)),p$499 ->  [reduction of 80 by [160]]
 189 : pbeta(A,subst(B,s(C),lift(D,0))),pbeta(E,subst(F,C,D)) -> pbeta(app(abs(A),E),subst(subst(B,0,F),C,D)),s(C)=<0 [chaining of 75 from 68]
 196 + p$499,!A,B,C.((0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)and pbeta(w,x)=>pbeta(subst(w,A,B),subst(x,A,C)))) and pbeta(u,v) [negative chaining of 83 from 84]
 197 + p$499,!A,B,C.((0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)=>pbeta(subst(w,A,B),subst(x,A,C)))) and pbeta(u,v) [reduction of 196 by [101,L]]
 198 + p$488,p$499                                         [expansion from 197]
 199 + p$488 -> !A,B,C.((0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)=>pbeta(subst(w,A,B),subst(x,A,C)))) [expansion from 197]
 200 + p$488 -> pbeta(u,v)                                 [expansion from 197]
 201 + p$488 -> (0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)=>pbeta(subst(w,A,B),subst(x,A,C))) [expansion from 199]
 202 + p$499,pbeta(u,v)                     [negative chaining of 198 from 200]
 203 + p$499,(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)=>pbeta(subst(w,A,B),subst(x,A,C))) [negative chaining of 198 from 201]
 204 + p$499,(0=<A and pbeta(B,C)=>pbeta(subst(u,A,B),subst(v,A,C)))and(0=<A and pbeta(B,C)=>pbeta(subst(w,A,B),subst(x,A,C))) [reduction of 203 by [202,L]]
 205 + p$487(A,B,C),p$499                                  [expansion from 204]
 206 + p$487(A,B,C) -> 0=<C and pbeta(A,B)=>pbeta(subst(u,C,A),subst(v,C,B)) [expansion from 204]
 207 + p$487(A,B,C) -> 0=<C and pbeta(A,B)=>pbeta(subst(w,C,A),subst(x,C,B)) [expansion from 204]
 208 + p$487(A,B,C),0=<C,pbeta(A,B) -> pbeta(subst(u,C,A),subst(v,C,B)) [expansion from 206]
 209 + p$487(A,B,C),pbeta(A,B) -> C<0,pbeta(subst(u,C,A),subst(v,C,B)) [totality resolution from 208]
 210 + p$487(A,B,C),0=<C,pbeta(A,B) -> pbeta(subst(w,C,A),subst(x,C,B)) [expansion from 207]
 211 + p$487(A,B,C),pbeta(A,B) -> C<0,pbeta(subst(w,C,A),subst(x,C,B)) [totality resolution from 210]
 216 + pbeta(subst(u,s(i),lift(s,0)),subst(v,s(i),lift(t,0))),pbeta(subst(w,i,s),subst(x,i,t)) -> s(i)=<0,p$496 [negative chaining of 189 from 88]
 217 + pbeta(subst(u,s(i),lift(s,0)),subst(v,s(i),lift(t,0))),pbeta(subst(w,i,s),subst(x,i,t)) -> p$496,s(i)=0 [reduction of 216 by [36,113]]
 218 + p$487(s,t,i),pbeta(s,t),pbeta(subst(u,s(i),lift(s,0)),subst(v,s(i),lift(t,0))) -> i<0,p$496,s(i)=0 [negative chaining of 211 from 217]
 219 + pbeta(subst(u,s(i),lift(s,0)),subst(v,s(i),lift(t,0))),p$487(s,t,i) -> s(i)=0,p$496 [reduction of 218 by [114,113,L]]
 220 + p$487(lift(s,0),lift(t,0),s(i)),pbeta(lift(s,0),lift(t,0)),p$487(s,t,i) -> s(i)<0,s(i)=0,p$496 [negative chaining of 209 from 219]
 221 + p$487(lift(s,0),lift(t,0),s(i)),pbeta(lift(s,0),lift(t,0)),p$487(s,t,i) -> s(i)=<0,p$496 [condensement of 220]
 222 + p$487(s,t,i),p$487(lift(s,0),lift(t,0),s(i)) -> p$496,s(i)=0 [reduction of 221 by [71,114,36,113]]
 223 + p$487(s,t,i) -> p$499,p$496,s(i)=0   [negative chaining of 205 from 222]
 224 + p$499,s(i)=0                            [reduction of 223 by [205,86,L]]
 225 + i<0,p$499                                      [chaining of 11 from 224]
 243 + p$499                                 [reduction of 225 by [113,86,L,L]]
 244 + !A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) and pbeta(u,v)=>0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))=>pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))),0=<k=>0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)) ->  [reduction of 161 by [243]]
 245 + p$486,0=<k=>0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)) ->  [expansion from 244]
 246 + p$486,!A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) and pbeta(u,v) [expansion from 244]
 247 + 0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))=>pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))) -> p$486 [expansion from 244]
 248 + p$485,p$486 ->                                      [expansion from 245]
 250 + 0=<i and pbeta(s,t)=>pbeta(subst(var(k),i,s),subst(var(k),i,t)) -> p$485 [expansion from 245]
 251 + p$484,p$486                                         [expansion from 246]
 252 + p$484 -> !A,B,C.(0=<A and pbeta(B,C)and pbeta(u,v)=>pbeta(subst(u,A,B),subst(v,A,C))) [expansion from 246]
 253 + p$484 -> pbeta(u,v)                                 [expansion from 246]
 254 + p$484,pbeta(u,v),0=<A,pbeta(B,C) -> pbeta(subst(u,A,B),subst(v,A,C)) [expansion from 252]
 255 + p$484,pbeta(u,v),pbeta(A,B) -> C<0,pbeta(subst(u,C,A),subst(v,C,B)) [totality resolution from 254]
 256 + p$483 -> p$486                                      [expansion from 247]
 257 + p$483,0=<i and pbeta(s,t)and pbeta(abs(u),abs(v))   [expansion from 247]
 258 + pbeta(abs(subst(u,s(i),lift(s,0))),abs(subst(v,s(i),lift(t,0)))) -> p$483 [expansion from 247]
 259 + p$482 -> p$485                                      [expansion from 250]
 260 + p$482,0=<i and pbeta(s,t)                           [expansion from 250]
 261 + pbeta(subst(var(k),i,s),subst(var(k),i,t)) -> p$482 [expansion from 250]
 262 + p$481,p$483                                         [expansion from 257]
 263 + p$481 -> 0=<i and pbeta(s,t)                        [expansion from 257]
 265 + p$491,p$482                                         [expansion from 260]
 267 + p$486,pbeta(u,v)                     [negative chaining of 251 from 253]
 269 + p$483,0=<i and pbeta(s,t)            [negative chaining of 262 from 263]
 270 + p$491,p$483                                         [expansion from 269]
 271 + pbeta(subst(var(k),i,s),var(k)) -> i=<k,p$482 [negative chaining of 59 from 261]
 273 + pbeta(subst(var(k),i,s),var(p(k))) -> k=<i,p$482 [negative chaining of 58 from 261]
 277 + p$482,i=<k                                 [reduction of 271 by [59,43]]
 278 + p$482,k=i                              [reduction of 273 by [58,43,277]]
 280 + pbeta(subst(var(k),i,s),subst(var(i),i,t)) -> p$482,p$482 [negative chaining of 278 from 261]
 283 + pbeta(subst(var(k),i,s),subst(var(i),i,t)) -> p$482 [condensement of 280]
 284 + pbeta(s,t) -> p$482                    [reduction of 283 by [15,278,15]]
 290 + pbeta(subst(u,s(i),lift(s,0)),subst(v,s(i),lift(t,0))) -> p$483 [negative chaining of 40 from 258]
 297 + p$484,pbeta(A,B) -> p$486,pbeta(subst(u,C,A),subst(v,C,B)),C<0 [negative chaining of 267 from 255]
 298 + pbeta(A,B) -> C<0,pbeta(subst(u,C,A),subst(v,C,B)),p$486 [reduction of 297 by [251]]
 300 + pbeta(lift(s,0),lift(t,0)) -> p$486,s(i)<0,p$483 [negative chaining of 298 from 290]
 303 + pbeta(lift(s,0),lift(t,0)) -> p$486,s(i)<0 [reduction of 300 by [256,L]]
 304 + pbeta(s,t) -> p$486,s(i)<0            [negative chaining of 71 from 303]
 313 + p$491,p$485                          [negative chaining of 265 from 259]
 314 + p$491,p$486                          [negative chaining of 270 from 256]
 315 + p$486 -> p$491                       [negative chaining of 313 from 248]
 316 + p$491                                        [reduction of 315 by [314]]
 317 + 0=<i                                         [reduction of 111 by [316]]
 318 + pbeta(s,t)                                   [reduction of 112 by [316]]
 325 + p$482                                        [reduction of 284 by [318]]
 327 + p$486                               [reduction of 304 by [318,36,317,L]]
 328 + p$485                                        [reduction of 259 by [325]]
 329 + false                                    [reduction of 248 by [328,327]]

Length = 157, Depth = 35



Total time: 27480 milliseconds

Number of forward inferences: 130
Number of tableau inferences: 60
Number of kept clauses: 216
*/