Benchmark Mined+Modified input to PINS Pruning by PINS PINS #iter/ time(s) #Axioms Axioms

Run length Run length 225→ 1 7 / 26s 0 - In-place Run length In-place Run length 230→ 1 7 / 36s 0 - LZ77 LZ77 225→ 1 6 / 1810s 0 - LZW LZW 231→ 1 4 / 150s 15 15 axioms over string ops: strlen, substr, bit2str, charAt, appendChar

Sum i Sum i 215→ 1 4 / 1s 0 - Scale Scale 216→ 1 3 / 4s 1 ∀ a,b,c,d: (a*c=b ∧ d=1/c) ⇒ a = b*d Shift Shift 216→ 1 3 / 4s 0 - Rotate Rotate 216→ 1 3 / 40s 1 ∀ x,y,X,Y,x',y': ( x' = x.cos(t)-y.sin(t) ∧ y' = x.sin(t)+y.cos(t) ∧ X = x'.cos(t)+y'.sin(t) ∧ Y = y'.cos(t)-x'.sin(t) ) ⇒ x=X ∧ y=Y

UUEncode UUEncode 220→ 1 7 / 34s 3 ∀ k,s1,s2 : pair(k, encode(s1,s2)) != footer ∀ k,s1,s2 : f=fst(pair(k,encode(s1,s2))) ⇒ f=k ∀ x,d,len,start : (x<len∧d=decode(snd(pair(len,encode(A[start],len))))) ⇒ get(d,x) = A[start+x] Base64 Base64 237→ 1 12 / 1377s 3 ∀ e,d : ( d=decode(cat(cat(cat(cat(null,get(e,0)),get(e,1)),pad),pad)) ∧ e=encode(cat(null,y)) ) ⇒ ( y=get(d,0)!=pad get(d,1)=get(d,2)=pad ) ∀ e,d : ( d=decode(cat(cat(cat(cat(null,get(e,0)),get(e,1)),get(e,2)),pad)) ∧ e=encode(cat(cat(null,y0),y1)) ) ⇒ ( y0=get(d,0)!=pad y1=get(d,1)!=pad get(d,2)=pad ) ∀ e,d : ( d=decode(cat(cat(cat(cat(null,get(e,0)),get(e,1)),get(e,2)),get(e,3))) ∧ e=encode(cat(cat(cat(null,y0),y1),y2)) ) ⇒ ( y0=get(d,0)!=pad y1=get(d,1)!=pad y2=get(d,2)!=pad ) Pkt Pkt 220→ 1 6 / 132s 2 ∀ e : size(e) ≥= 1 ∀ x,e,sz: x=memcpy(e,sz) ∧ sz=size(e) ⇒ e=memread(x,sz)