added interpolation

interpolation/Ex0_BasicConflict.p

@@ -0,0 +1,13 @@
+
+vampire(option,avatar,off).
+vampire(option,show_interpolant,new_heur).
+vampire(symbol,function,z,0,left).
+
+vampire(left_formula).
+  fof(fA,hypothesis,p(z)).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB, hypothesis,![X]:~p(X)).
+vampire(end_formula).
+

interpolation/Ex0_BasicConflict_NoLocalProof.p

@@ -0,0 +1,14 @@
+
+vampire(option,avatar,off).
+vampire(option,show_interpolant,new_opt).
+vampire(symbol,function,c,0,left).
+vampire(symbol,function,d,1,right).
+
+vampire(left_formula).
+  fof(fA,hypothesis,![Y]:p(c,Y)).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB, hypothesis,![X]:~p(X,d(X))).
+vampire(end_formula).
+

interpolation/Ex1_Arithmetic_UinterpretedFCT_Interp.p

@@ -0,0 +1,43 @@
+% A: z < 0 AND x <= z AND y <= x 
+% B: y <= 0 AND x + y >= 0
+
+vampire(option,avatar,off).
+
+% vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+vampire(option,show_interpolant,new_opt).
+
+vampire(symbol,function,z,0,left).
+
+fof(geq1,axiom,
+    ~greater(Y,X) <=> greater(X,Y) | X = Y).
+fof(greater1,axiom,
+    greater(X,Y) => X != Y).
+
+fof(greater2,axiom,
+    greater(s(X),X)).
+
+fof(greater_transitive,axiom,
+    greater(X,Y) & greater(Y,Z) => greater(X,Z)).
+
+fof(a,axiom,(  one=s(zero)  )).
+
+fof(a,axiom,(  plus(X,zero)=X  )).
+fof(a,axiom,(  plus(X,Y)=Z <=> minus(Z,Y)=X  )).
+fof(a,axiom,(  plus(X,Y)=plus(Y,X)  )).
+fof(a,axiom,(  plus(X,Z)=plus(Y,Z) <=> X=Y )).
+fof(a,axiom,(  plus(X,s(Y))=s(plus(X,Y))  )).
+fof(a,axiom,(  (greater(X,Z) & ~greater(zero,Y)) => greater(plus(X,Y),Z)  )).
+fof(a,axiom,(  (~greater(Z,X) & ~greater(zero,Y)) => ~greater(Z,plus(X,Y))  )).
+fof(a,axiom,(  greater(plus(X,Y),Y) <=> greater(X,zero)  )).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( greater(zero, z) & ~greater(x,z) & ~greater(y,x) )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB1,hypothesis,( ~greater(zero, plus(x,y)) )).
+  fof(fB2,hypothesis,( ~greater(y,zero) )).
+vampire(end_formula).
+

interpolation/Ex2_Arithmetic_UinterpretedFCT_Interp.p

@@ -0,0 +1,46 @@
+% A: g(a) = c + 5 AND f(g(a)) >= c + 1
+% B: h(b) = d + 4 AND d = c + 1 AND f(h(b)) < c+ 1.
+
+vampire(option,avatar,off).
+
+% vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+vampire(option,show_interpolant,new_opt).
+
+vampire(symbol,function,g,1,left).
+vampire(symbol,function,a,0,left).
+
+vampire(symbol,function,h,1,right).
+vampire(symbol,function,b,0,right).
+
+fof(geq1,axiom,
+    ~greater(Y,X) <=> greater(X,Y) | X = Y).
+fof(greater1,axiom,
+    greater(X,Y) => X != Y).
+
+fof(greater2,axiom,
+    greater(s(X),X)).
+
+fof(greater_transitive,axiom,
+    greater(X,Y) & greater(Y,Z) => greater(X,Z)).
+
+fof(a,axiom,(  one=s(zero)  )).
+
+fof(a,axiom,(  plus(X,zero)=X  )).
+fof(a,axiom,(  plus(X,Y)=Z <=> minus(Z,Y)=X  )).
+fof(a,axiom,(  plus(X,Y)=plus(Y,X)  )).
+fof(a,axiom,(  plus(X,Z)=plus(Y,Z) <=> X=Y )).
+fof(a,axiom,(  plus(X,s(Y))=s(plus(X,Y))  )).
+fof(a,axiom,(  (greater(X,Z) & ~greater(zero,Y)) => greater(plus(X,Y),Z)  )).
+fof(a,axiom,(  (~greater(Z,X) & ~greater(zero,Y)) => ~greater(Z,plus(X,Y))  )).
+fof(a,axiom,(  greater(plus(X,Y),Y) <=> greater(X,zero)  )).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( g(a)=plus(c, s(s(s(s(s(zero))))) ) & ~greater(plus(c,one),f(g(a))) )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB,hypothesis,( h(b)=plus(d, s(s(s(s(zero)))) ) & d=plus(c,one) & greater(plus(c,one),f(h(b))) )).
+vampire(end_formula).
+

interpolation/Ex3_Arithmetic_UinterpretedFCT_Interp.p

@@ -0,0 +1,43 @@
+% A: p<=c AND c<=q AND f(c)=1
+% B: q<=d AND d<=p AND f(d)=0
+
+vampire(option,avatar,off).
+
+% vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+vampire(option,show_interpolant,new_opt).
+
+vampire(symbol,function,c,0,left).
+vampire(symbol,function,d,0,right).
+
+fof(geq1,axiom,
+    ~greater(Y,X) <=> greater(X,Y) | X = Y).
+fof(greater1,axiom,
+    greater(X,Y) => X != Y).
+
+fof(greater2,axiom,
+    greater(s(X),X)).
+
+fof(greater_transitive,axiom,
+    greater(X,Y) & greater(Y,Z) => greater(X,Z)).
+
+fof(a,axiom,(  one=s(zero)  )).
+
+fof(a,axiom,(  plus(X,zero)=X  )).
+fof(a,axiom,(  plus(X,Y)=Z <=> minus(Z,Y)=X  )).
+fof(a,axiom,(  plus(X,Y)=plus(Y,X)  )).
+fof(a,axiom,(  plus(X,Z)=plus(Y,Z) <=> X=Y )).
+fof(a,axiom,(  plus(X,s(Y))=s(plus(X,Y))  )).
+fof(a,axiom,(  (greater(X,Z) & ~greater(zero,Y)) => greater(plus(X,Y),Z)  )).
+fof(a,axiom,(  (~greater(Z,X) & ~greater(zero,Y)) => ~greater(Z,plus(X,Y))  )).
+fof(a,axiom,(  greater(plus(X,Y),Y) <=> greater(X,zero)  )).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( ~greater(p,c) & ~greater(c,q) & f(c)=one )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB,hypothesis,( ~greater(q,d) & ~greater(d,p) & f(d)=zero )).
+vampire(end_formula).
+

interpolation/Ex4_Quantified_Interp.p

@@ -0,0 +1,23 @@
+% A: Q(f(a)) AND  NOT(Q(f(b)))
+% B: f(V)=c
+
+vampire(option,avatar,off).
+
+% vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+vampire(option,show_interpolant,new_opt).
+
+vampire(symbol,predicate,q,1,left).
+vampire(symbol,function,a,0,left).
+vampire(symbol,function,b,0,left).
+vampire(symbol,function,c,0,right).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( q(f(a)) & ~q(f(b)) )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB,hypothesis,![V]:( f(V)=c )).
+vampire(end_formula).
+

interpolation/Ex5_UninterpretedFCT_Interp.p

@@ -0,0 +1,23 @@
+% A: (a = c) AND (f(c) = a) 
+% B: (c = b) AND  NOT(b = f(c)). 
+
+
+vampire(option,avatar,off).
+
+% vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+vampire(option,show_interpolant,new_opt).
+
+
+vampire(symbol,function,a,0,left).
+vampire(symbol,function,b,0,right).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( a=c & f(c)=a )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB,hypothesis,( c=b & b!=f(c) )).
+vampire(end_formula).
+

interpolation/Ex6_List_Interp.p

@@ -0,0 +1,26 @@
+% A: c2=car(c1) AND c3=cdr(c1) AND NOT(atom(c1))
+% B: NOT(c1) = cons(c2,c3)
+
+
+vampire(option,avatar,off).
+
+% vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+vampire(option,show_interpolant,new_opt).
+
+%colors
+vampire(symbol,function,car,1,left).
+vampire(symbol,function,cdr,1,left).
+vampire(symbol,function,atom,1,left).
+
+% \forall x,y,z: Not(atom(x)) => cons(car(x),cdr(x))=x
+fof(a,axiom,( ~atom(X) => cons(car(X),cdr(X))=X )).
+
+vampire(left_formula).
+  fof(fA,hypothesis,( c2=car(c1) & c3=cdr(c1) & ~atom(c1) )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB,hypothesis,( c1!=cons(c2,c3) )).
+vampire(end_formula).
+

interpolation/Ex7_Arithmetic_UinterpretedFCT_Interp.p

@@ -0,0 +1,44 @@
+% A: (f(x1) + x2 = x3) AND  (f(y1) + y2 = y3) AND  (y1 <= x1)
+% B: (x2 = g(b)) AND (y2 = g(b)) AND (x1 <= y1) AND (x3 < y3)
+
+vampire(option,avatar,off).
+
+vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+% vampire(option,show_interpolant,new_opt).
+
+vampire(symbol,function,f,1,left).
+vampire(symbol,function,g,1,right).
+vampire(symbol,function,b,0,right).
+
+fof(geq1,axiom,
+    ~greater(Y,X) <=> greater(X,Y) | X = Y).
+fof(greater1,axiom,
+    greater(X,Y) => X != Y).
+
+fof(greater2,axiom,
+    greater(s(X),X)).
+
+fof(greater_transitive,axiom,
+    greater(X,Y) & greater(Y,Z) => greater(X,Z)).
+
+fof(a,axiom,(  one=s(zero)  )).
+
+fof(a,axiom,(  plus(X,zero)=X  )).
+fof(a,axiom,(  plus(X,Y)=Z <=> minus(Z,Y)=X  )).
+fof(a,axiom,(  plus(X,Y)=plus(Y,X)  )).
+fof(a,axiom,(  plus(X,Z)=plus(Y,Z) <=> X=Y )).
+fof(a,axiom,(  plus(X,s(Y))=s(plus(X,Y))  )).
+fof(a,axiom,(  (greater(X,Z) & ~greater(zero,Y)) => greater(plus(X,Y),Z)  )).
+fof(a,axiom,(  (~greater(Z,X) & ~greater(zero,Y)) => ~greater(Z,plus(X,Y))  )).
+fof(a,axiom,(  greater(plus(X,Y),Y) <=> greater(X,zero)  )).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( plus(f(x1),x2)=x3 & plus(f(y1),y2)=y3 & ~greater(y1,x1) )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fA,hypothesis,( x2=g(b) & y2=g(b) & ~greater(x1,y1) & greater(y3,x3) )).
+vampire(end_formula).
+

interpolation/Ex8_Array_Interp.p

@@ -0,0 +1,38 @@
+% A: True AND a'[x']=y AND x'=x AND y'=y+1 AND z'=x'
+% B: NOT(a'[z'] = y'-1)
+
+vampire(option,avatar,off).
+
+vampire(option,show_interpolant,old).
+% vampire(option,show_interpolant,new_heur).
+% vampire(option,show_interpolant,new_opt).
+
+vampire(symbol,function,y,0,left).
+vampire(symbol,function,x,0,left).
+vampire(symbol,function, x1,0,left).
+
+fof(greater1,axiom,
+    greater(X,Y) => X != Y).
+
+fof(greater2,axiom,
+    greater(s(X),X)).
+
+fof(greater_transitive,axiom,
+    greater(X,Y) & greater(Y,Z) => greater(X,Z)).
+
+fof(a,axiom,(  one=s(zero)  )).
+
+fof(a,axiom,(  plus(X,zero)=X  )).
+fof(a,axiom,(  plus(X,Y)=Z <=> minus(Z,Y)=X  )).
+fof(a,axiom,(  plus(X,Y)=plus(Y,X)  )).
+fof(a,axiom,(  plus(X,s(Y))=s(plus(X,Y))  )).
+
+
+vampire(left_formula).
+  fof(fA,hypothesis,( a1(x1)=y & x1=x & y1=plus(y,one) & z1=x1 )).
+vampire(end_formula).
+
+vampire(right_formula).
+  fof(fB,conjecture, a1(z1)=minus(y1,one) ).
+vampire(end_formula).
+