From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sat, 10 Feb 2024 02:22:14 +0100 Subject: Initial commit --- test/golden/inductive/encoding tasks.golden | 170 ++++++++++++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 test/golden/inductive/encoding tasks.golden (limited to 'test/golden/inductive/encoding tasks.golden') diff --git a/test/golden/inductive/encoding tasks.golden b/test/golden/inductive/encoding tasks.golden new file mode 100644 index 0000000..2e9a2d5 --- /dev/null +++ b/test/golden/inductive/encoding tasks.golden @@ -0,0 +1,170 @@ +fof(fin,conjecture,elem(emptyset,pow(fA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(fin,conjecture,(elem(fa,fA)&elem(fB,pow(fA)))=>elem(cons(fa,fB),pow(fA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(fin_mono,conjecture,subseteq(fin(fA),fin(fB))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +fof(fin_mono1,axiom,subseteq(fA,fB)). +------------------ +fof(tracl,conjecture,elem(fw,fR)=>elem(fw,times(fld(fR),fld(fR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(tracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(quasirefltracl,conjecture,elem(fa,fld(fR))=>elem(pair(fa,fa),times(fld(fR),fld(fR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(quasirefltracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(refltracl,conjecture,elem(fa,fA)=>elem(pair(fa,fa),times(fA,fA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(refltracl,conjecture,(elem(pair(fa,fb),times(fA,fA))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fA,fA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(acc,conjecture,![Xxa,Xxb]:(subseteq(Xxa,Xxb)=>subseteq(pow(Xxa),pow(Xxb)))). +fof(refltracl,axiom,![Xa,Xb,XA,XR,Xc]:((elem(pair(Xa,Xb),refltracl(XA,XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),refltracl(XA,XR)))). +fof(refltracl,axiom,![Xa,XA,XR]:(elem(Xa,XA)=>elem(pair(Xa,Xa),refltracl(XA,XR)))). +fof(refltracl,axiom,![XA,XR]:subseteq(refltracl(XA,XR),times(XA,XA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). +------------------ +fof(acc,conjecture,(elem(fa,fld(fR))&elem(preimg(fR,cons(fa,emptyset)),pow(fld(fR))))=>elem(fa,fld(fR))). +fof(refltracl,axiom,![Xa,Xb,XA,XR,Xc]:((elem(pair(Xa,Xb),refltracl(XA,XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),refltracl(XA,XR)))). +fof(refltracl,axiom,![Xa,XA,XR]:(elem(Xa,XA)=>elem(pair(Xa,Xa),refltracl(XA,XR)))). +fof(refltracl,axiom,![XA,XR]:subseteq(refltracl(XA,XR),times(XA,XA))). +fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). +fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). +fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). +fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). +fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). +fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). +fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). +fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). +fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). +fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). +fof(fld,axiom,![XR]:fld(XR)=emptyset). +fof(times,axiom,![XA,XB]:times(XA,XB)=emptyset). +fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). +fof(pow,axiom,![XA]:pow(XA)=emptyset). +fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). \ No newline at end of file -- cgit v1.2.3