%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% $Id: leantest.pl,v 1.1 2012/11/15 00:14:20 beckert Exp $
% Sicstus Prolog
% Copyright (C) 1993: Bernhard Beckert & Joachim Posegga
%                     Universit"at Karlsruhe
%                     Email: {beckert|posegga}@mail.informatik.kit.edu
%
% Purpose:            Testdata for \LeanTaP
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



:- module(leantest,[provefml/1,incprovefml/1,uv_provefml/1,uv_incprovefml/1]).
:- op(400,fy,-), op(500,xfy,&), op(600,xfy,v),op(650,xfy,=>), op(700,xfy,<=>).

:- 	use_module(leantap,[prove/2,prove_uv/2]).
:- 	use_module(nnf,[nnf/2]).

:- 	use_module(library(lists),[member/2]).


% ------------------------------------------------------------
%
% provefml(Name)
% calls fml(Name,Limit,Fml) and tries to prove Fml with VarLim = Limit.
%
% use 'provefml(_),fail.' to prove all formulae in the database


provefml(Name) :-
	fml(Name,Limit,F),
	write(Name),
	nnf(F,NNF),
	statistics(runtime,[_,_]),
	(prove(NNF,Limit)
	   -> (statistics(runtime,[_,Time]),
	       format(' proved in ~w msec, VarLim = ~w ~n',[Time,Limit]))
           ; (statistics(runtime,[_,Time]),
              format(' no proof after ~w msec. ~n',[Time]))).

% ------------------------------------------------------------
%
% incprovefml(Name)
% same as provefml/1, but VarLimit is determined by iterative deepening
%
% 'incprovefml(_),fail.' runs over all problems in the database

incprovefml(Name) :-
	fml(Name,_,F),
	write(Name),
	nnf(F,NNF),
	statistics(runtime,[_,_]),
	(prove(NNF,Limit)
	   -> (statistics(runtime,[_,Time]),
	     format('  proved in ~w msec, found VarLim = ~w ~n',[Time,Limit]))
           ; (statistics(runtime,[_,Time]),
              format(' no proof after ~w msec. ~n',[Time]))).

% ------------------------------------------------------------
%
% uv_provefml(Name)
% calls fml(Name,Limit,Fml) and tries to prove Fml with VarLim = Limit
% and universal variables
%
% use 'uv_provefml(_),fail.' to prove all formulae in the database


uv_provefml(Name) :-
	fml(Name,Limit,F),
	write(Name),
	nnf(F,NNF),
	statistics(runtime,[_,_]),
	(prove_uv(NNF,Limit)
	   -> (statistics(runtime,[_,Time]),
	       format(' proved in ~w msec, VarLim = ~w ~n',[Time,Limit]))
           ; (statistics(runtime,[_,Time]),
              format(' no proof after ~w msec. ~n',[Time]))).

% ------------------------------------------------------------
%
% uv_incprovefml(Name)
% same as uv_provefml/1, but VarLimit is determined by iterative deepening
%
% 'uv_incprovefml(_),fail.' runs over all problems in the database

uv_incprovefml(Name) :-
	fml(Name,_,F),
	write(Name),
	nnf(F,NNF),
	statistics(runtime,[_,_]),
	(prove_uv(NNF,Limit)
	   -> (statistics(runtime,[_,Time]),
	     format('  proved in ~w msec, found VarLim = ~w ~n',[Time,Limit]))
           ; (statistics(runtime,[_,Time]),
              format(' no proof after ~w msec. ~n',[Time]))).


%%%%%%%%%% DATABASE OF PELLETIER:

% ---------------------------------------------------------
% fml(?Name,?VarLim,?Fml)
%
% stores formula Fml under Name with VarLim.
%
% This database consists of a subset of Pelletier's formulae
	

fml(pel1,0,-((p => q) <=> (-q => -p))).

fml(pel2,0,-(-(-p) <=> p)).

fml(pel3,0,-(-(p => q) => (q => p))).

fml(pel4,0,-((-p => q) <=> (-q => p))).

fml(pel5,0,-(((p v q) => (p v r)) => (p v (q => r)))).

fml(pel6,0,-(p v -p)).

fml(pel7,0,-(p v -(-(-p)))).

fml(pel8,0,-(((p => q) => p) => p)).

fml(pel9,0,-((((p v q) & (-p v q)) & (p v -q)) => -(-p v -q))).

fml(pel10,0,-(p <=> q) & 
  (q => r) & 
  (r => (p & q)) & 
  (p => (q v r))).

 
fml(pel11,0,-(p <=> p)).


fml(pel12,0,-(((p <=> q) <=> r) <=> (p <=> (q <=> r)))).


fml(pel13,0,-((p v (q & r)) <=> ((p v q) & (p v r)))).


fml(pel14,0,-((p <=> q) <=> ((q v -p) & (-q v p)))).


fml(pel15,0,-((p => q) <=> (-p v q))).


fml(pel16,0,-((p => q) v (q => p))).


fml(pel17,0,-(((p & (q => r)) => s) <=> (((-p v q) v s) & ((-p v -r) v s)))).


fml(pel18,2,-ex(Y, all(X, (f(Y) => f(X))))).


fml(pel19,2,-ex(X, all(Y, all(Z, ((p(Y) => q(Z)) => (p(X) => q(X))))))).


fml(pel20,6,-(all(X, all(Y, ex(Z, all(W, ((p(X) & q(Y)) => (r(Z) & s(W))))))) => ex(X1, ex(Y1, ((p(X1) & q(Y1)) => ex(Z1, (r(Z1)))))))).


fml(pel21,2,-ex(X, (p <=> f(X))) & 
  ex(X1, (p => f(X1))) & 
  ex(X2, (f(X2) => p))).

 
fml(pel22,2,-(all(X, (p <=> f(X))) => (p <=> all(X1, (f(X1)))))).


fml(pel23,1,-(all(X, (p v f(X))) <=> (p v all(X1, (f(X1)))))).


fml(pel24,6,-ex(X, (p(X) & r(X))) & 
  -ex(X1, (s(X1) & q(X1))) & 
  all(X4, (p(X4) => (q(X4) v r(X4)))) & 
  (-ex(X2, (p(X2))) => ex(Y, (q(Y)))) & 
  all(X3, ((q(X3) v r(X3)) => s(X3)))).

 
fml(pel25,3,-ex(X, (q(X) & p(X))) & 
  ex(X1, (p(X1))) & 
  all(X2, (f(X2) => (-g(X2) & r(X2)))) & 
  all(X3, (p(X3) => (g(X3) & f(X3)))) & 
  (all(X4, (p(X4) => q(X4))) v ex(Z, (p(Z) & r(Z))))).

 
fml(pel26,3,-(all(X, (p(X) => r(X))) <=> all(Y, (q(Y) => s(Y)))) & 
  (ex(X1, (p(X1))) <=> ex(Y2, (q(Y2)))) & 
  all(X2, all(Y3, ((p(X2) & q(Y3)) => (r(X2) <=> s(Y3)))))).

 
fml(pel27,4,-all(X, (j(X) => -i(X))) & 
  ex(X1, (f(X1) & -g(X1))) & 
  all(X2, (f(X2) => h(X2))) & 
  all(X4, ((j(X4) & i(X4)) => f(X4))) & 
  (ex(X5, (h(X5) & -g(X5))) => all(X6, (i(X6) => -h(X6))))).

 
fml(pel28,3,-all(X, ((p(X) & f(X)) => g(X))) & 
  all(X1, (p(X1) => all(Z, (q(Z))))) & 
  (all(X2, (q(X2) v r(X2))) => ex(X21, (q(X21) & s(X21)))) & 
  (ex(X3, (s(X3))) => all(X31, (f(X31) => g(X31))))).

 
fml(pel29,2,-((all(X, (f(X) => h(X))) & all(U, (g(U) => j(U)))) <=> all(W, all(Y, ((f(W) & g(Y)) => (h(W) & j(Y)))))) & 
  (ex(X1, (f(X1))) & ex(Y1, (g(Y1))))).

 
fml(pel30,2,-all(X, (i(X))) & 
  all(X1, ((f(X1) v g(X1)) => -h(X1))) & 
  all(X2, ((g(X2) => -i(X2)) => (f(X2) & h(X2))))).

 
fml(pel31,3,-ex(X, (i(X) & j(X))) & 
  -ex(X1, (f(X1) & (g(X1) v h(X1)))) & 
  ex(X2, (i(X2) & f(X2))) & 
  all(X3, (-h(X3) => j(X3)))).

 
fml(pel32,3,-all(X, ((f(X) & k(X)) => j(X))) & 
  all(X1, ((f(X1) & (g(X1) v h(X1))) => i(X1))) & 
  all(X2, ((i(X2) & h(X2)) => j(X2))) & 
  all(X3, (k(X3) => h(X3)))).

 
fml(pel33,1,-(all(X, ((p(a) & (p(X) => p(b))) => p(c))) <=> all(X1, ((-p(a) v (p(X1) v p(c))) & (-p(a) v (-p(b) v p(c))))))).


fml(pel34,5,-((ex(X, all(Y, (p(X) <=> p(Y)))) <=> (ex(U, (q(U))) <=> all(W, (q(W))))) <=> (ex(X1, all(Y1, (q(X1) <=> q(Y1)))) <=> (ex(U1, (p(U1))) <=> all(W1, (p(W1))))))).


fml(pel35,4,-ex(X, ex(Y, (p(X,Y) => all(Z, all(W, (p(Z,W)))))))).


fml(pel36,6,-all(X, ex(Y, (h(X,Y)))) & 
  all(X1, ex(Y2, (f(X1,Y2)))) & 
  all(X2, ex(Y1, (g(X2,Y1)))) & 
  all(X3, all(Y3, ((f(X3,Y3) v g(X3,Y3)) => all(Z3, ((f(Y3,Z3) v g(Y3,Z3)) => h(X3,Z3))))))).

 
fml(pel37,7,-all(X, ex(Y, (r(X,Y)))) & 
  all(Z, ex(W, all(X1, ex(Y1, (p(X1,Z) => ((p(Y1,W) & p(Y1,Z)) & (p(Y1,W) => ex(U, (q(U,W)))))))))) & 
  all(X2, all(Z2, (-p(X2,Z2) => ex(Y2, (q(Y2,Z2)))))) & 
  (ex(X3, ex(Y3, (q(X3,Y3)))) => all(Z3, (r(Z3,Z3))))).

 
fml(pel38,4,-(all(X, ((p(a) & (p(X) => ex(Y, (p(Y) & r(X,Y))))) => ex(Z, ex(W, ((p(Z) & r(X,W)) & r(W,Z)))))) <=> all(X1, ((((-p(a)) v p(X1)) v ex(Z1, ex(W1, ((p(Z1) & r(X1,W1)) & r(W1,Z1))))) & (((-p(a)) v (-ex(Y1, (p(Y1) & r(X1,Y1))))) v ex(Z2, ex(W2, ((p(Z2) & r(X1,W2)) & r(W2,Z2))))))))).


fml(pel39,1,ex(X, all(Y, (f(Y,X) <=> -f(Y,Y))))).


fml(pel40,3,-(ex(Y, all(X, (f(X,Y) <=> f(X,X)))) => -all(X1, ex(Y1, all(Z, (f(Z,Y1) <=> -f(Z,X1))))))).


fml(pel41,3,ex(Z, all(X, (f(X,Z)))) & 
  all(Z1, ex(Y, all(X1, (f(X1,Y) <=> (f(X1,Z1) & -f(X1,X1))))))).

 
fml(pel42,3,ex(Y, all(X, (f(X,Y) <=> -ex(Z, (f(X,Z) & f(Z,X))))))).


fml(pel43,5,-all(X,all(Y, ((q(X,Y) => q(Y,X)) & (q(Y,X) => q(X,Y))))) & 
  all(X1,all(Y1,(q(X1,Y1) => all(Z, ((f(Z,X1) => f(Z,Y1)) & (f(Z,Y1) => f(Z,X1))))))) & 
  all(X2,all(Y2,(all(Z2, ((f(Z2,X2) => f(Z2,Y2)) & (f(Z2,Y2) => f(Z2,X2)))) => q(X2,Y2))))).

 
fml(pel44,3,-ex(X, (j(X) & -f(X))) & 
  all(X1, (f(X1) => (ex(Y, (g(Y) & h(X1,Y))) & ex(Y1, (g(Y1) & -h(X1,Y1)))))) & 
  ex(X2, (j(X2) & all(Y2, (g(Y2) => h(X2,Y2)))))).

 
fml(pel45,5,-ex(X, (f(X) & -ex(Y, (g(Y) & h(X,Y))))) & 
  all(X1, ((f(X1) & all(Y, ((g(Y) & h(X1,Y)) => j(X1,Y)))) => all(Y1, ((g(Y1) & h(X1,Y1)) & k(Y1))))) & 
  -ex(Y2, (l(Y2) & k(Y2))) & 
  ex(X2, ((f(X2) & all(Y3, (h(X2,Y3) => l(Y3)))) & all(Y11, ((g(Y11) & h(X2,Y11)) => j(X2,Y11)))))).

 
fml(pel46,5,-all(X, (f(X) => g(X))) & 
  all(X1,all(Y,(f(X1) & ((f(Y) & h(Y,X1)) => g(Y)) => g(X1)))) & 
  (ex(X2, (f(X2) & -g(X2))) => ex(X21, ((f(X21) & -g(X21)) & all(Y2, ((f(Y2) & -g(Y2)) => j(X21,Y2)))))) & 
  all(X3,all(Y3,((f(X3) & f(Y3) & h(X3,Y3)) => -j(Y3,X3))))).

fml(pel47,44,((-(ex(X1,ex(Y1,(animal(X1) & animal(Y1) & ex(Z1,(isagrain(Z1) & likestoeat(Y1,Z1)) & likestoeat(X1,Y1)))))))

 & all(X2,(wolf(X2)        => animal(X2))) & ex(X3,wolf(X3))
 & all(X4,(fox(X4)         => animal(X4))) & ex(X5,fox(X5))
 & all(X6,(bird(X6)        => animal(X6))) & ex(X7,bird(X7))
 & all(X8,(caterpillar(X8) => animal(X8))) & ex(X9,caterpillar(X9))
 & all(X10,(snail(X10)     => animal(X10))) & ex(X11,snail(X11))

 & ex(X12,isagrain(X12)) & all(X13,(isagrain(X13) => isaplant(X13)))

 & all(X14,(animal(X14) => (all(Y2,isaplant(Y2) => likestoeat(X14,Y2)) v
                      all(Y3,((animal(Y3) & smaller(Y3,X14) & ex(Z1,(isaplant(Z1) & likestoeat(Y3,Z1)))) =>
                              likestoeat(X14,Y3))))))

 & all(X15,all(Y4,((bird(Y4) & (snail(X15) v caterpillar(X15))) => smaller(X15,Y4))))
 & all(X16,all(Y5,((bird(X16) & fox(Y5)) => smaller(X16,Y5))))
 & all(X17,all(Y6,((fox(X17)  & wolf(Y6)) => smaller(X17,Y6))))
 & all(X18,all(Y7,((wolf(X18) & (fox(Y7) v isagrain(Y7))) => -likestoeat(X18,Y7))))
 & all(X19,all(Y8,((bird(X19) & caterpillar(Y8)) => likestoeat(X19,Y8))))
 & all(X20,all(Y9,((bird(X20) & snail(Y9)) => -likestoeat(X20,Y9))))
 & all(X21,((caterpillar(X21) v snail(X21)) => ex(Y10,(isaplant(Y10) & likestoeat(X21,Y10)))))
)).



% The following are some of the problems from Overbeek's CADE-11 competition.

fml(overbeek1,19,
    ((-p(a,b,c)) &
    p(b,a,c) &
    all(X,p(X,X,e)) &
    all(X,all(Y,p(X,Y,f(X,Y)))) &
    all(X,p(X,g(X),e)) &
    all(X,p(g(X),X,e)) &
    all(X,p(X,e,X)) &
    all(X,p(e,X,X)) &
    all(X,all(Y,all(Z,all(U,all(V,all(W,(
         (p(X,Y,U) & p(Y,Z,V) & p(U,Z,W)) => p(X,V,W)))))))) &
    all(X,all(Y,all(Z,all(U,all(V,all(W,(
         (p(X,Y,U) & p(Y,Z,V) & p(X,V,W)) => p(U,Z,W)))))))) &
    all(X,all(Y,all(U,all(V,
         (p(X,Y,U) & p(X,Y,V)) => eq(U,V))))) &
    all(X,eq(X,X)) &
    all(X,all(Y,(eq(X,Y) => eq(Y,X)))) &
    all(X,all(Y,all(Z,((eq(X,Y) & eq(Y,Z)) => eq(X,Z))))) &
    all(X,all(Y,all(U,all(V,((eq(U,V) & p(U,X,Y)) => p(V,X,Y)))))) &
    all(X,all(Y,all(U,all(V,((eq(U,V) & p(X,U,Y)) => p(X,V,Y)))))) &
    all(X,all(Y,all(U,all(V,((eq(U,V) & p(X,Y,U)) => p(X,Y,V)))))) &
    all(X,all(U,all(V,(eq(U,V) => eq(f(X,U),f(X,V)))))) &
    all(X,all(U,all(V,(eq(U,V) => eq(f(U,X),f(V,X)))))) &
    all(U,all(V,(eq(U,V) => eq(g(U),g(V))))))
).

fml(overbeek2,10,(
    p(a,b,c) &
    p(c,g(a),d) &
    p(d,g(b),h) &
    p(h,b,j) &
    p(j,g(h),k) &
   -p(k,g(b),e) &
    all(X,all(Y,(p(X,X,Y) => p(X,Y,e)))) &
    all(X,all(Y,(p(X,X,Y) => p(Y,X,e)))) &
    all(X,all(Y,p(X,Y,f(X,Y)))) &
    all(X,p(X,g(X),e)) &
    all(X,p(g(X),X,e)) &
    all(X,p(X,e,X)) &
    all(X,p(e,X,X)) &
    all(X,all(Y,all(Z,all(U,all(V,all(W,(
         (p(X,Y,U) & p(Y,Z,V) & p(U,Z,W)) => p(X,V,W)))))))) &
    all(X,all(Y,all(Z,all(U,all(V,all(W,(
         (p(X,Y,U) & p(Y,Z,V) & p(X,V,W)) => p(U,Z,W)))))))) &
    all(X,all(Y,all(U,all(V,
         (p(X,Y,U) & p(X,Y,V)) => eq(U,V))))) &
    all(X,eq(X,X)) &
    all(X,all(Y,(eq(X,Y) => eq(Y,X)))) &
    all(X,all(Y,all(Z,((eq(X,Y) & eq(Y,Z)) => eq(X,Z))))) &
    all(X,all(Y,all(U,all(V,((eq(U,V) & p(U,X,Y)) => p(V,X,Y)))))) &
    all(X,all(Y,all(U,all(V,((eq(U,V) & p(X,U,Y)) => p(X,V,Y)))))) &
    all(X,all(Y,all(U,all(V,((eq(U,V) & p(X,Y,U)) => p(X,Y,V)))))) &
    all(X,all(U,all(V,(eq(U,V) => eq(f(X,U),f(X,V)))))) &
    all(X,all(U,all(V,(eq(U,V) => eq(f(U,X),f(V,X)))))) &
    all(U,all(V,(eq(U,V) => eq(g(U),g(V))))))
).

fml(overbeek4,14,(
    all(X,all(Y,all(Z,p(e(X,e(e(Y,e(Z,X)),e(Z,Y))))))) &
    -p(e(e(e(a,e(b,c)),c),e(b,a))) &
    all(X,all(Y,((p(X) & p(e(X,Y))) => p(Y))))
)).